SmpSL Verification Conditions Generator
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 FO2BD
FO2BD is the two-variable fragment extended with bounded domains. Bounded domains are fixed finite sets. FO2BD extends FO2 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 FO2BD formula which does not quantify over the bounded domains is a FO2 formula. FO2BD 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 s1 ∀b s2 ((s1 = s2) ∨ ~T(x,y,s1) ∨ ~T(x,y,s2)The quantifier ∀d ranges over the unbounded domain. The quantifier ∀b ranges over b.
For a more detailed explanation of FO2BD 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 r1 r2 …)
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 FO2BD 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 FO2BD 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 FO2 sentence compatible with FO2-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.