[More Detail] [Collapse All]
Feature: Verify correctness invariants

TLA+ invariants are used to verify that application correctenss is
not violated.

This feature demonstrates three scenarios:

1) correct implementation & correcness check pass
2) in-correct implementation, which is found using correcness check
3) in-correct implementation, which is correcness check fails to identify
   (false-positive)
features/003-example/060-verify-correcness.feature
- Background:
link

Define interface operation '/customer(post)', which accepts
customer data with id and name properties. Extend domains to
have cardinality 6.

Extend interface operation '/customer(post)' to implement service
as a macro 'customer_post'. This macro updates entries in state
variable 'customers'.

Customer data is validated using operator 'Valid_customer', and
invariant 'Verify_customers' verifies that all entries in state
variable 'customer' pass 'Valid_customer' check.
features/003-example/060-verify-correcness.feature:15
Given I successfully run `sbuilder.rb init`
And I successfully run `sbuilder.rb extend`
And a file named "cnf/sbuilder.yaml" with:
#
# Define interfaces

interfaces:
    -  className: Sbuilder::ParamSetLoaderSwagger
       file: public_interface.yaml
And a file named "cnf/public_interface.yaml" with:
#
#  Define application interface /customer(post)
#
swagger: "2.0"
info:
   version: 1.0.0
   title: TLA-sbuilder demo application public interface
host: localhost
basePath: /api
schemes:
    - http
consumes:
    - application/json
produces:
   - application/json
paths:
 /customer:
   post: 
     operationId: postCustomer
     parameters:
       - name: customer
         in: body
         description: Customers to enter
         required: true
         schema:
             $ref: '#/definitions/Customer'
     responses:
        200:
           description: OK
definitions: 
   Customer:
        properties:
          id:
           type: string
          name:
           type: string
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define resolver in file example_resolver.yaml

resolvers:
      - url: cnf/example_resolver.yaml
Given a file named "cnf/example_resolver.yaml" with:
#
# Resolver uses catch-all matcher. Particularly, it matches also
# parameter set for interface operation '/customer(post)'. Domain
# rules maps domain for operation parameters 'id', 'name', and use
# catch-all rule for all other parameter names.
#
-    Name: default-relsover
     Matcher: !ruby/regexp /.*/
     Rules: 
      - Matcher: id
        Domain: id_domain
      - Matcher: name
        Domain: name_domain
      - Matcher: !ruby/regexp /.*/
        Domain: default_domain
Given a file named "cnf/common-setup.yaml" with:
# define implementation for  interface '/customer(post)'
- interface-extension:
   - matcher: /customer(post)
     implementation: customer_post

# define cardinalities
#
- domain-extension:
    - domain: id_domain
      cardinality: 3
    - domain: name_domain
      cardinality: 3
And I append to "src/state" with:
(* Initialize state variable 'customers' to empty set *)
customers = {} 
And I append to "src/operator" with:
\* Customer must have non-Nil name
Valid_customer( customer ) == customer.name # Nil
Given I append to "src/correctness" with:
\* Verify that all entries in 'customers' -state variable are valid
Verify_customers == \A customer \in customers : Valid_customer( customer )
And YAML configuration file `cnf/sbuilder.yaml`
#
# Activate INVARIANT directive in setup.tla

invariants:
      - Verify_customers: Verify that all entries in customers -state variable are valid
- Scenario: Correct implementation - verification passed
link

In this scenario, '/customer(post)' service validates input before
updating database.  Correctness invariant 'Verify_customers', is
not violated, when environment calls interface '/customer(post)',
and tries all input combinations.
features/003-example/060-verify-correcness.feature:161
Given I append to "src/interface" with:
\* Correct implementation: check that customer is valid before db-entry
macro customer_post( input ) {
        if ( Valid_customer( input.customer ) ) {
           customers := customers \union { input.customer }
        }
}
And YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    extensions:
      -  url: cnf/common-setup.yaml
      -  url: cnf/all-inputs.yaml
And a file named "cnf/all-inputs.yaml" with:
# setup step-extesion makes a call to interface '/customer(post)',
# and passes all input combinations to the interface.
#
- step-extension:
     - interface: /customer(post)
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Model checking completed. No error has been found."
- Scenario: In-correct implementation - verification failure found using specific input value
link


In this scenario, '/customer(post)' service does not validate
input before updating database.

Correctness invariant 'Verify_customers', is violated, and
verification run reveal the error, it calls interface
'/customer(post)', and tries all input combinations.
features/003-example/060-verify-correcness.feature:205
Given I append to "src/interface" with:
   macro customer_post( input ) {
        \* ERROR: should validate entry before db-update
        customers := customers \union { input.customer }
   }
And YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: example
    extensions:
      -  url: cnf/common-setup.yaml
      -  url: cnf/all-inputs.yaml
Given a file named "cnf/all-inputs.yaml" with:
# setup step-extesion makes a call to interface '/customer(post)',
# and passes all input combinations to the interface.
#
- step-extension:
     - interface: /customer(post)
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Invariant Verify_customers is violated."
- Scenario: In correct implementation - false-positive
link

In this scenario, '/customer(post)' service does not validate
input before updating database.

However, setup 'false-positive' does not reveal this problem,
because no environment does customer name with Nil value to the
interface '/customer(post)'
features/003-example/060-verify-correcness.feature:250
Given I append to "src/interface" with:
   macro customer_post( input ) {
        \* ERROR: should validate entry before db-update
        customers := customers \union { input.customer }
   }
And YAML configuration file `cnf/sbuilder.yaml`
setups:
  - setupDirectory: false-positive
    extensions:
      -  url: cnf/common-setup.yaml
      -  url: cnf/non-nil-inputs.yaml
Given a file named "cnf/non-nil-inputs.yaml" with:

# Make to calls to /customer(post). First call uses domain value
# 1, and second domain value 2. Domain value 0(=Nil) is not sent
# to the interface, and correctness invariant 'Verify_customers'
# does not detect the problem.

- step-extension:
     - interface: /customer(post)
       input:
          customer:
              name: 1
     - interface: /customer(post)
       input:
          customer:
              name: 2
When I successfully run `sbuilder.rb generate false-positive`
And I cd to "gen/false-positive/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I successfully run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Model checking completed. No error has been found."