The tool SmpSL Verification Conditions Generator receives as input a SmpSL program with its specification and computes the verification condition.

The language SmpSL

SmpSL is a simple script language with the embedded SQL commands SELECT, INSERT, UPDATE, and DELETE based on arXiv:1610.02101. See Section 3 of arXiv:1610.02101 for the definition of the language.

The specification logic FO²_BD

FO²_BD is the two-variable fragment extended with bounded domains. Bounded domains are fixed finite sets. FO²_BD extends FO² by allowing quantification on an unbounded number of variables, under the restriction that all variables aside from two range over the bounded domains only. Two variables may range over the unbounded domain. A FO²_BD formula which does not quantify over the bounded domains is a FO² formula. FO²_BD imposes the restriction on the vocabulary that every relation has at most two columns ranging over the unbounded domain.

For example, assume we have one bounded domain: b = {true, false}. The following sentence says that the first two columns of T form the key of T.

(∀_d x ∀_d y ∀_b s₁ ∀_b s₂ ((s₁ = s₂) ∨ ~T(x,y,s₁) ∨ ~T(x,y,s₂)

The quantifier ∀_d ranges over the unbounded domain. The quantifier ∀_b ranges over b.

For a more detailed explanation of FO²_BD and more examples see Sections 3.3.3 and Section 2 of arXiv:1610.02101

Input of SmpSL VC generator

The input file to our tool consists of four sections:

• The list of tables
• a precondition following the keyword requires,
• the program, and
• a postcondition following the keyword ensures.

List of tables

It is a list of expressions of the form:

• (TableName i)
• (TableName i BOUNDED r₁ r₂ …)

i is either 1 or 2. i indicates the number of columns ranging over the unbounded domain. After the keyword BOUNDED are the sizes of the bounded domains for any additional column.

For instance, (Users 1) (Subscriptions 2) indicates that the database has two tables, one table with a single column (column1) and the other with two columns (column1 and column2), all of which range over the unbounded domains. Another example: (Papers 2 BOUNDED 3 4) (Authors 2) (Conflicts 2) indicates there are three tables. Papers has four columns, column1 and column2 ranging over the unbounded domain, and b0 and b1 ranging over domains of sizes 3 and 4 respectively.

Precondition

The precondition is of the form:
requires F
where F is an FO²_BD sentence.

For instance:

requires exists nl (~(nl = newsletter) & forall y (Users(y) -> Subscriptions(nl, y)))

Note that we do not indicate whether variables range over bounded or unbounded domains neither in the name of the variable nor in the quantifier. A variable may take any name (including but not limited to x and y), and its type (unbounded/bounded domain) is determined by its usage according to the types of the columns.

Another example:

(Papers 2 BOUNDED 3 5) (Authors 2) (Conflicts 2) (ReviewerBids 2)  (Reviewers 2 BOUNDED 2)  (ReviewerAssignments  2) (Out 1 BOUNDED 5)

requires forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &
forall x y (Out(x,y) <-> exists z w (Papers(x, z, w, y) & Authors(currentUser, x)))

Program

The program consists of SELECT, INSERT, UPDATE, DELETE and if commands. Some examples of programs:

INSERT INTO Subscriptions VALUES (newsletter,user) ; 

if (IsNotEmpty(SELECT G.Column1 FROM G WHERE Column1 = bidId))
  INSERT INTO ReviewerBids VALUES (currentUser, bidId);
else
  skip ;

UPDATE Out SET b0 = 0:5 WHERE b0 = 2:5 OR b0 = 3:5 OR b0 = 4:5;

Postcondition

The postcondition is of the form:
requires F
where F is an FO²_BD sentence. F has the same format as in the precondition.

Examples of input files

(Users 1) (Subscriptions 2)

requires 
exists x (~(x = newsletter) & forall y (Users(y) -> Subscriptions(x, y)))

INSERT INTO Subscriptions VALUES (newsletter,user) ;

ensures 
forall u (Users(u) -> exists x (Subscriptions(x, u)))

(Papers 2 BOUNDED 3 3) (Authors 2) (Conflicts 2) (ReviewerBids 2)  (Reviewers 2 BOUNDED 2)  (ReviewerAssignments  2)

requires
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &&
ReviewerBids(reviewer, assignId)

INSERT INTO ReviewerAssignments VALUES (reviewer, assignId) ;

ensures
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y))

(Papers 2 BOUNDED 3 5) (Authors 2) (Conflicts 2) (ReviewerBids 2)  (Reviewers 2 BOUNDED 2)  (ReviewerAssignments  2) (Out 1 BOUNDED 5)

requires
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &&
forall x y (Out(x,y) <-> exists z w (Papers(x, z, w, y) & Authors(currentUser, x)))

UPDATE Out SET b0 = 0:5 WHERE b0 = 2:5 OR b0 = 3:5 OR b0 = 4:5;

ensures
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &&
forall title session (Out(title,session) -> (session = 0:5 || session = 1:5))

For more examples, see the benchmarks page.

Download

The source code in Java can be downloaded from here:

SmpSL VC generator (zip, 405.7KB)

Output

The tool outputs an smt2 file containing an FO² sentence compatible with FO²-solver and other solvers that receive smt2 format as input such as Z3 theorem prover. It is guaranteed that the only variables used in the output file are x and y.

An example of an output of the VC generator:

(declare-sort V 0)
(declare-datatypes () ((B$2 _0@2 _1@2) (B$3 _0@3 _1@3 _2@3)))
(declare-fun ReviewerBids (V V) Bool)
(declare-fun ReviewerAssignments (V V) Bool)
(declare-fun Authors (V V) Bool)
(declare-fun Papers (V V B$3 B$3) Bool)
(declare-fun Reviewers (V V B$2) Bool)
(declare-fun Conflicts (V V) Bool)
(declare-fun ReviewerBids_ (V V) Bool)
(declare-fun ReviewerAssignments_ (V V) Bool)
(declare-fun Authors_ (V V) Bool)
(declare-fun Papers_0_0 (V V) Bool)
(declare-fun Papers_0_1 (V V) Bool)
(declare-fun Papers_0_2 (V V) Bool)
(declare-fun Papers_1_0 (V V) Bool)
(declare-fun Papers_1_1 (V V) Bool)
(declare-fun Papers_1_2 (V V) Bool)
(declare-fun Papers_2_0 (V V) Bool)
(declare-fun Papers_2_1 (V V) Bool)
(declare-fun Papers_2_2 (V V) Bool)
(declare-fun Reviewers_0 (V V) Bool)
(declare-fun Reviewers_1 (V V) Bool)
(declare-fun Conflicts_ (V V) Bool)
(declare-const reviewer V)
(declare-const assignId V)
(assert (not (=> (and (and (forall ((x V)) (forall ((y V)) (=> (ReviewerBids x y) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (ReviewerAssignments x y) (not (Conflicts x y)))))) (ReviewerBids reviewer assignId)) (and (forall ((x V)) (forall ((y V)) (=> (ReviewerBids x y) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (or (ReviewerAssignments x y) (and (= x reviewer) (= y assignId))) (not (Conflicts x y)))))))) )
(check-sat)
(get-model)

For more examples, see the benchmarks page.