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 s1b 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.

Latest News

Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30. The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) […]

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Helmut Veith Stipend

The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated […]

Continue reading

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Full news archive