# 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 FO^{2}_{BD}

FO^{2}_{BD} is the two-variable fragment extended with bounded domains. Bounded domains are fixed finite sets. FO^{2}_{BD} extends FO^{2} 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^{2}_{BD} formula which does not quantify over the bounded domains is a FO^{2} formula. FO^{2}_{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_{1}∀_{b}s_{2}((s_{1}= s_{2}) ∨ ~T(x,y,s_{1}) ∨ ~T(x,y,s_{2})

The quantifier ∀_{d} ranges over the unbounded domain. The quantifier ∀_{b} ranges over b.

For a more detailed explanation of FO^{2}_{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
_{1}r_{2}…)

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^{2}_{BD} sentence.

For instance:

requiresexists 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)requiresforall 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^{2}_{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^{2} sentence compatible with FO^{2}-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.