The RISC Algorithm Language (RISCAL)

Tutorial and Reference Manual

(Version 1.0.14)

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC)

Johannes Kepler University, Linz, Austria

Wolfgang.Schreiner@risc.jku.at

January 15, 2018

Abstract

This report documents the RISC Algorithm Language (RISCAL). RISCAL is a language

and associated software system for describing (potentially nondeterministic) mathematical

algorithms over discrete structures, formally specifying their behavior by logical formulas

(program annotations in the form of preconditions, postconditions, and loop invariants),

and formulating the mathematical theories (by deﬁning functions and predicates and stating

theorems) on which these speciﬁcations depend. The language is based on a type system that

ensures that all variable domains are ﬁnite; nevertheless the domain sizes may depend on

unspeciﬁed numerical constants. By instantiating these constants with values, all algorithms,

functions, and predicates become executable, and all formulas become decidable. Indeed the

RISCAL software implements a (parallel) model checker that allows to verify the correctness

of algorithms and the associated theories with respect to their speciﬁcations for all possible

input values of the parameter domains.

1

Contents

1 Introduction 4

2 A Quick Start 5

3 More Examples 17

4 Related Work 26

5 Future Work 28

A The Software System 32

A.1 Installing the Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

A.2 Running the Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

A.3 The User Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

A.4 Distributed Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

B The Speciﬁcation Language 41

B.1 Lexical and Syntactic Structure . . . . . . . . . . . . . . . . . . . . . . . . . . 42

B.2 Speciﬁcations and Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . 44

B.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

B.2.2 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

B.2.3 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

B.3 Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

B.3.1 Declarations and Assignments . . . . . . . . . . . . . . . . . . . . . . 48

B.3.2 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

B.3.3 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

B.3.4 Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

B.3.5 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

B.4 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

B.5 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

B.5.1 Constants and Applications . . . . . . . . . . . . . . . . . . . . . . . . 55

B.5.2 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

B.5.3 Equalities and Inequalities . . . . . . . . . . . . . . . . . . . . . . . . 57

B.5.4 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

B.5.5 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

B.5.6 Tuples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

B.5.7 Records . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

B.5.8 Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

B.5.9 Maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

B.5.10 Recursive Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

B.5.11 Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

B.5.12 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

B.5.13 Binders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

2

B.5.14 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

B.5.15 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

B.6 Quantiﬁed Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

B.7 ANTLR 4 Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

C Example Speciﬁcations 71

C.1 Euclidean Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

C.2 Insertion Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

C.3 DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

C.4 DPLL Algorithm with Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . 76

3

1 Introduction

The formal veriﬁcation of computer programs is a very challenging task. If the program operates

on an unbounded domain of values, the only general veriﬁcation technique is to generate,

from the text of the program and its speciﬁcation, veriﬁcation conditions, i.e., logical formulas

whose validity ensures the correctness of the program with respect to its speciﬁcation. The

generation of such conditions generally requires from the human additional program annotations

that express meta-knowledge about the program such as loop invariants and termination measures.

Since for more complex programs proofs of these formulas by fully automatic reasoners rarely

succeed, typically interactive proving assistants are applied where the human helps the software

to construct successful proofs.

This may become a frustrating task, because usually the ﬁrst veriﬁcation attempts are doomed

to fail: the veriﬁcation conditions are often not valid due to (also subtle) deﬁciencies in the

program, its speciﬁcation, or annotations. The main problem is then to ﬁnd out whether a proof

fails because of an inadequate proof strategy or because the condition is not valid and, if the

later is the case, which errors make the formula invalid. Typically, therefore most time and eﬀort

in veriﬁcation is actually spent in attempts to prove invalid veriﬁcation conditions, often due to

inadequate annotations, in particular due to loop invariants that are too strong or too weak.

For this reason, programs are often restricted to make fully automatic veriﬁcation feasible that

copes without extra program annotations and without manual proving eﬀorts. One possibility

is to restrict the domain of a program such that it only operates on a ﬁnite number of values,

which allows to apply model checkers that investigate all possible executions of a program.

Another possibility is to limit the length of executions being considered; then bounded model

checkers (typically based on SMT solvers, i.e., automatic decision procedures for combinations

of decidable logical theories) are able to check the correctness of a program for a subset of

the executions. However, while being fully automatic, (bounded) model checking is time- and

memory-consuming, and ultimately does not help to verify the general correctness of a program

operating on unbounded domains with executions of unbounded length.

Based on prior expertise with computer-supported program veriﬁcation, also in educational

scenarios [27, 22], we have started the development of RISCAL (RISC Algorithm Language) as

an attempt to make program veriﬁcation less painful. The term “algorithm language” indicates

that RISCAL is intended to model, rather than low-level code, high-level algorithms as can be

found in textbooks on discrete mathematics [25]. RISCAL thus provides a rich collection of data

types (e.g., sets and maps) and operations (e.g., quantiﬁed formulas as Boolean conditions and

implicit deﬁnitions of values by formulas) but only cares about the correctness of execution, not

its eﬃciency. The core idea behind RISCAL is to use automatic techniques to ﬁnd problems in

a program, its speciﬁcation, or its annotations, that may prevent a successful veriﬁcation before

actually attempting to prove veriﬁcation conditions; we thus aim to start a proof of veriﬁcation

conditions only when we are reasonably conﬁdent that they are indeed valid.

As a ﬁrst step towards this goal, RISCAL restricts in a program P all program variables and

mathematical variables to ﬁnite types where the number of values of a type T, however, may

depend on an unspeciﬁed constant n ∈ N. If we set n to some concrete value c, we get an

instance P

c

of P where all speciﬁcations and annotations can be eﬀectively evaluated during the

execution of the program (runtime assertion checking). Furthermore, we can execute a program

4

and check the annotations for all possible inputs (model checking); only if we do not ﬁnd errors,

the veriﬁcation of the general program P may be attempted. The current version of the RISCAL

software documented in this report thus supports model checking of ﬁnite domain instances of

programs via the runtime assertion checking of all possible executions, which is based on the

executability of all speciﬁcations and annotations (further mechanisms will be added in time).

The RISCAL software is freely available as open source under the GNU General Public

License, Version 3 at

https://www.risc.jku.at/research/formal/software/RISCAL

with this document included in electronic form as the manual for the software.

The remainder of this document is organized as follows: Section 2 represents a tutorial into

the practical use of the RISCAL language and system based on a concrete example of a RISCAL

speciﬁcation. Section 3 elaborates more examples to deepen the understanding. Section 4 relates

our work to prior research; Section 5 elaborates our plans for the future evolution of RISCAL.

Appendix A provides a detailed documentation for the use of the system. Appendix B represents

the reference manual for the speciﬁcation language. Appendix C gives the full source of the

speciﬁcations used in the tutorial; this source is also included in the distribution.

2 A Quick Start

We start with a quick overview on the RISCAL speciﬁcation language and associated software

system whose graphical user interface is depicted in Figure 1 (an enlarged version is shown in

Figure 3 on page 36).

System Overview The system is started from the command line by executing

RISCAL &

The user interface is divided into two parts. The left part mainly embeds an editor panel with

the current speciﬁcation. The right part is mainly ﬁlled by an output panel that shows the output

of the system when analyzing the speciﬁcation that is currently loaded in the editor. The top of

both parts contains some interactive elements for controlling the editor respectively the analyzer.

Appendix A.3 explains the user interface in more detail.

The system remembers across invocations the last speciﬁcation ﬁle loaded into the editor, i.e.,

when the software is started, the speciﬁcation used in the last invocation is automatically loaded.

Likewise the options selected in the right panel are remembered across invocations. However,

a button (Reset System) in the right panel allows to reset the system to a clean state (no

speciﬁcation loaded and all options set to their default values).

Speciﬁcations are written as plain text ﬁles in Unicode format (UTF-8 encoding) with arbitrary

ﬁle name extension (e.g., .txt). The RISCAL language uses several Unicode characters that

cannot be found on keyboards, but for each such character there exists an equivalent string in

ASCII format that can be typed on a keyboard. While the RISCAL grammar supports both

alternatives, the use of the Unicode characters yields much prettier speciﬁcations and is thus

recommended. The RISCAL editor can be used to translate the ASCII string to the Unicode

5

Figure 1: The RISCAL User Interface

character by ﬁrst typing the string and then (when the editor caret is immediately to the right of

this string) pressing <Ctrl>-#, i.e, the Control key and simultaneously the key depicting #. Also

later such textual replacements can be performed by positioning the editor caret to the right of

the string and pressing <Ctrl>-#. The current table of replacements is given in Appendix B.1.

Whenever a speciﬁcation is loaded from disk respectively saved to disk after editing, it is

immediately processed by a syntax checker and a type checker. Error messages are displayed

in the output panel; the positions of errors are displayed by red markers in the editor window;

moving the mouse pointer over such a marker also displays the corresponding error message.

Speciﬁcation Language As a ﬁrst example of the speciﬁcation language (which is deﬁned

in Appendix B), we write a speciﬁcation consisting of a mathematical theory of the greatest

common divisor and its computation by the Euclidean algorithm. This speciﬁcation (whose full

content is given in Appendix C.1) starts with the declarations

val N: N;

type nat = N[N];

that introduce a natural number constant N a type nat that consists of the values 0, . . . , N (the

symbol N may be entered as Nat followed by pressing the keys <Ctrl>-#) which corresponds

to the mathematical deﬁnition

nat := {x ∈ N | x ≤ N}.

6

The value of N is not deﬁned in the speciﬁcation but in the RISCAL software. We may enter

this value either in the ﬁeld “Default Value” in the right part of the window or we may open with

the button “Other Values” a window that allows to set diﬀerent values for diﬀerent constants; if

there is no entry for a speciﬁc constant, the “Default Value” is used.

The speciﬁcation deﬁnes then a predicate

pred divides(m:nat,n:nat) ⇔ ∃p:nat. m·p = n;

which corresponds to the mathematical deﬁnition

divides ⊆ nat × nat

divides(m, n) :⇔ ∃p ∈ nat. m · p = n

In other words, divides(m, n) means “m divides n” which is typically written as m|n.

We then introduce the “greatest common divisor” function as

fun gcd(m:nat,n:nat): nat

requires m , 0 ∨ n , 0;

= choose result:nat with

divides(result,m) ∧ divides(result,n) ∧

¬∃r:nat. divides(r,m) ∧ divides(r,n) ∧ r > result;

This function is deﬁned by an implicit deﬁnition; for any m ∈ nat and n ∈ nat with m , 0 or

n , 0, its result is the largest value result ∈ nat that divides both m and n.

The function can be used to deﬁne some other values, e.g.

val g:nat = gcd(N,N-1);

which corresponds to the mathematical deﬁnition

g ∈ nat, g := gcd(N, N − 1)

This function satisﬁes certain general properties stated as follows:

theorem gcd0(m:nat) ⇔ m,0 ⇒ gcd(m,0) = m;

theorem gcd1(m:nat,n:nat) ⇔ m , 0 ∨ n , 0 ⇒ gcd(m,n) = gcd(n,m);

theorem gcd2(m:nat,n:nat) ⇔ 1 ≤ n ∧ n ≤ m ⇒ gcd(m,n) = gcd(m%n,n);

Each such “theorem” is represented by a named predicate which is implicitly claimed to be true

for all possible applications, corresponding to the mathematical propositions

∀m ∈ nat. m , 0 ⇒ gcd(m, 0) = m

∀m ∈ nat, n ∈ nat. m , 0 ∨ n , 0 ⇒ gcd(m, n) = gcd(n, m)

∀m ∈ nat, n ∈ nat. 1 ≤ n ∧ n ≤ m ⇒ gcd(m, n) = gcd(m mod n, n)

The symbol % thus stands for the mathematical “modulus” operator (arithmetic remainder).

Now we write a procedure gcdp that implements the Euclidean algorithm:

7

proc gcdp(m:nat,n:nat): nat

requires m , 0 ∨ n , 0;

ensures result = gcd(m,n);

{

var a:nat := m;

var b:nat := n;

while a > 0 ∧ b > 0 do

invariant gcd(a,b) = gcd(old_a,old_b);

decreases a+b;

{

if a > b then

a := a%b;

else

b := b%a;

}

return if a = 0 then b else a;

}

The clauses requires and ensures state that for any arguments m, n with m , 0 or n , 0

(i.e., for any argument that satisﬁes the given precondition), the result of this procedure (denoted

by the keyword result) is indeed the greatest common divisor of m and n, as speciﬁed above

(i.e., the result satisﬁes the given postcondition). The invariant states the crucial property for

proving the correctness of the algorithm: before and after every iteration of the loop, the greatest

common divisor of the current values of program variables a and b equals the greatest common

divisor of their initial values (denoted by the keyword preﬁx old_), i.e., the greatest divisor of

m and n. The clause decreases states the crucial property for the termination of the algorithm:

the value a + b decreases by every loop iteration but does not become negative. While all these

loop annotations are not necessary for executing the algorithm, they formally express additional

knowledge that aid our understanding of the algorithm.

Above procedure demonstrates that RISCAL incorporates an algorithmic language with the

usual programming language constructs. However, unlike a classical programming language,

this algorithm language allows also nondeterministic executions as in the following procedure:

proc main(): ()

{

choose m:nat, n:nat with m , 0 ∨ n , 0;

print m,n,gcdp(m,n);

}

This procedure does not return a value (indicated by the return type ()) but just prints the

arguments and result of some application of procedure gcdp. The argument values m, n for its

application are not uniquely determined: the choose command selects for m and n some values

in nat such that at least one of them is not zero.

Language Features As shown above, a RISCAL speciﬁcation may contain deﬁnitions of

8

• types,

• constants, functions, predicates,

• theorems, and

• procedures

which may depend on (declared but) undeﬁned natural number constants. Functions may be ex-

plicitly deﬁned or implicitly speciﬁed by predicates, theorems are special predicates that always

yield “true”, procedures may contain apart from the usual algorithmic constructs also nondeter-

ministic choices, and functions and procedures may be annotated with pre- and postconditions

respectively loop invariants and termination measures. The language does not distinguish be-

tween logical terms and formulas, a formula is just a term of a type Bool and a predicate is a

function with that result type.

Furthermore, there is no diﬀerence between logical formulas and conditions in program

constructs; every logical formula may be in a procedure for example used as a loop condition.

Likewise, there is no diﬀerence between logical terms and program expressions; every logical

term may be for example used on the right hand side of an assignment statement. Procedures

have (apart from potential output) no other eﬀect than returning values (also the procedure main

above implicitly returns a value ()); they may be thus also used as functions in logical formulas.

The RISCAL language has been designed in such a way that

• every type has only ﬁnitely many values, and thus

• every language construct is executable, and thus

• every constant, function, predicate, theorem, procedure can be evaluated.

For instance, the truth value of a formula like

∃p:nat. m·p = n

can be determined by evaluating, for every possible nat-value p, the formula m · p = n. If there is

at least one value for which this equality holds, the formula is true, otherwise it is false. Likewise,

the function

fun gcd(m:nat,n:nat): nat

requires m , 0 ∨ n , 0;

= choose result:nat with ...

can be evaluated by enumerating all possible candidate values for the result of the function.

The function result is then one such candidate for which the condition “. . . ” holds (if this is

not the case for any candidate, the execution may abort with an error message). Therefore also

all function/predicate/procedure annotations requires, ensures, invariant, and decreases

are executable.

In summary, every RISCAL speciﬁcation is completely executable; in particular, all stated

claims (theorems and function/predicate/procedure annotations) are checkable.

9

Execution and Model Checking Whenever a speciﬁcation ﬁle is loaded or saved (or when

the button is saved), the corresponding speciﬁcation is processed,i.e., checked for syntactic and

type errors (with graphical markers displaying the locations of the errors) and translated into

an executable representation. For this purpose, the value of every constant introduced by a val

clause on the top level of a speciﬁcation is determined: if a natural number constant c is just

declared, the value of c is taken from the user interface, either from the panel “Other Values”or

(if this panel does not list a value for c) from the box “Default Value”. If the value of a constant is

deﬁned by a term, this value is determined by evaluating the term (which may contain arbitrary

computations including the application of user-deﬁned functions). The values of constants may

be used as bounds in types; a speciﬁcation is thus always processed for a speciﬁc set of values for

the global constants (if the user changes the values, the speciﬁcation is automatically re-processed

before execution). In our example speciﬁcation, we may thus get the output

RISC Algorithm Language 1.0 (March 1, 2017)

http://www.risc.jku.at/research/formal/software/RISCAL

(C) 2016-, Research Institute for Symbolic Computation (RISC)

This is free software distributed under the terms of the GNU GPL.

Execute "RISCAL -h" to see the available command line options.

-----------------------------------------------------------------

Reading file /home/schreine/papers/RISCALManual2017/gcd.txt

Using N=3.

Computing the value of g...

Type checking and translation completed.

which indicates that the user provided the value 3 for constant N and that the value of g was

computed by evaluating the deﬁnition.

After the processing of a speciﬁcation, the menu “Operation” lists all operations together with

their argument types (operations with diﬀerent argument types may have the same name). We

may e.g. select the operation main() which selects the method

proc main(): ()

{

choose m:nat, n:nat with m , 0 ∨ n , 0;

print m,n,gcdp(m,n);

}

By pressing the button (Start Execution) the system executes main() which produces (as-

suming that option Nondeterminism has not been selected) the output

Executing main().

Run of deterministic function main():

0,1,1

Result (34 ms): ()

Execution completed (96 ms).

Not all nondeterministic branches may have been considered.

10

The system has thus chosen the values 0 for m and 1 for n and computed their greatest common

divisor 1.

However, if we select the option Nondeterminism and then press the button , the speciﬁ-

cation is ﬁrst re-processed and then executed with the following output:

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (11 ms): ()

Branch 1 of nondeterministic function main():

0,2,2

Result (24 ms): ()

Branch 2 of nondeterministic function main():

0,3,3

Result (11 ms): ()

...

Branch 13 of nondeterministic function main():

3,2,1

Result (8 ms): ()

Branch 14 of nondeterministic function main():

3,3,3

Result (8 ms): ()

Branch 15 of nondeterministic function main():

No more results (434 ms).

Execution completed (441 ms).

Thus the program was executed for all possible choices for m and n subject to the condition

m , 0 ∨ n , 0 and computed the greatest common divisor. In this execution, all annotations

speciﬁed in requires, ensures, invariant, and decreases have been checked by evaluating

the corresponding formulas respectively terms, thus also evaluating the implicitly deﬁned function

gcd and the predicate divides. For instance, changing the postcondition of gcdp to

ensures result = 1;

yields output

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (6 ms): ()

Branch 1 of nondeterministic function main():

ERROR in execution of main(): evaluation of

ensures result = 1;

at line 24 in file gcd.txt:

postcondition is violated

ERROR encountered in execution.

11

which demonstrates that the second execution of main violated the speciﬁcation. Likewise,

setting the termination measure to

decreases a;

produces the output

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (10 ms): ()

...

Branch 4 of nondeterministic function main():

ERROR in execution of main(): evaluation of

decreases a;

at line 30 in file gcd.txt:

variant value 1 is not less than old value 1

ERROR encountered in execution.

However, rather than main in nondeterministic mode, we may also executed gcdp for all possible

inputs. We thus deselect “Nondeterminism” and select from the menu Operation the operation

gcdp(Z,Z), which yields the following execution:

Executing gcdp(Z,Z) with all 16 inputs.

Ignoring inadmissible inputs...

Run 1 of deterministic function gcdp(1,0):

Result (1 ms): 1

Run 2 of deterministic function gcdp(2,0):

Result (0 ms): 2

...

Run 15 of deterministic function gcdp(3,3):

Result (1 ms): 3

Execution completed for ALL inputs (206 ms, 15 checked, 1 inadmissible).

Not all nondeterministic branches may have been considered.

The system thus runs gcdp with all “admissible” inputs, i.e., with all argument tuples that satisfy

the speciﬁed precondition

requires m,0 ∨ n,0;

The system thus executes the operation (and checks all annotations) for 15 inputs excluding

the inadmissible input m = 0 and n = 0. The last line of the output reminds us that we have

executed the system in deterministic mode which is generally faster but does not consider all

possible execution branches resulting from nondeterministic choices such the one performed in

the deﬁnition of gcd.

By switching on the option “Silent”, the output is compacted to

12

Executing gcdp(Z,Z) with all 16 inputs.

Execution completed for ALL inputs (6 ms, 15 checked, 1 inadmissible).

Not all nondeterministic branches may have been considered.

which just gives the essential information.

Parallelism If we increase the value of N to say 60, checking all possible inputs may take some

time. We thus switch on the option “Multi-Threaded” and set “Threads” to 4. The system thus

applies 4 concurrent threads for the application of the operation which is (on a computer with 4

processor cores) much faster and yields output:

Executing gcdp(Z,Z) with all 3721 inputs.

PARALLEL execution with 4 threads (output disabled).

1336 inputs (955 checked, 1 inadmissible, 0 ignored, 380 open)...

2193 inputs (1812 checked, 1 inadmissible, 0 ignored, 380 open)...

3005 inputs (2629 checked, 1 inadmissible, 0 ignored, 375 open)...

3721 inputs (3445 checked, 1 inadmissible, 0 ignored, 275 open)...

Execution completed for ALL inputs (8826 ms, 3720 checked, 1 inadmissible).

Not all nondeterministic branches may have been considered.

The statistics output and the growing blue bar displayed on top of the output area displays the

progress of a longer running computation. To interrupt such an execution, we may press the

button (Stop Execution).

For even larger inputs, we may also set the option “Distributed” and and thus partially delegate

computations to other instances of the RISCAL software, possibly running on other computers

(e.g., high performance servers) running in the local network or being sited in other remote

networks to which we are connected by the Internet. For this, we also have conﬁgure the

connection information in menu “Servers” appropriately, see Appendix A.4 for details. The

output for N = 100 may then look as follows:

Executing gcdp(Z,Z) with all 10201 inputs.

Executing "/software/RISCAL/etc/runssh

qftquad2.risc.jku.at 4"...

Connecting to qftquad2.risc.uni-linz.ac.at:52387...

Executing "/software/RISCAL/etc/runmach 4"...

Connecting to localhost:9999...

Connected to remote servers.

PARALLEL execution with 4 local threads and 2 remote servers (output disabled).

939 inputs (544 checked, 1 inadmissible, 0 ignored, 394 open)...

2819 inputs (1117 checked, 1 inadmissible, 0 ignored, 1701 open)...

2819 inputs (1424 checked, 1 inadmissible, 0 ignored, 1394 open)...

4605 inputs (2851 checked, 1 inadmissible, 0 ignored, 1753 open)...

5327 inputs (3799 checked, 1 inadmissible, 0 ignored, 1527 open)...

6339 inputs (4779 checked, 1 inadmissible, 0 ignored, 1559 open)...

8035 inputs (6363 checked, 1 inadmissible, 0 ignored, 1671 open)...

13

8716 inputs (7408 checked, 1 inadmissible, 0 ignored, 1307 open)...

Execution completed for ALL inputs (18500 ms, 10200 checked, 1 inadmissible).

Not all nondeterministic branches may have been considered.

Here, in addition to four local threads, two remote servers are applied, one with Internet name

qftquad2.risc.uni-linz.ac.at; the other is called localhost because it is connected to

our process via a local proxy process that bypasses a ﬁrewall.

We may not only check procedures but also functions, relations, and especially theorems; in

the later case we check whether all applications of the theorem yield value “true”. For instance,

we may check the theorem gcd2(Z,Z) deﬁned as

theorem gcd2(m:nat,n:nat) ⇔ 1 ≤ n ∧ n ≤ m ⇒ gcd(m,n) = gcd(m%n,n);

for which the output

Executing gcd2(Z,Z) with all 10201 inputs.

PARALLEL execution with 4 threads (output disabled).

1904 inputs (1704 checked, 0 inadmissible, 0 ignored, 200 open)...

3757 inputs (3673 checked, 0 inadmissible, 0 ignored, 84 open)...

7372 inputs (6436 checked, 0 inadmissible, 0 ignored, 936 open)...

Execution completed for ALL inputs (7127 ms, 10201 checked, 0 inadmissible).

Not all nondeterministic branches may have been considered.

validates its correctness.

As demonstrated by above examples, the RISCAL software encompasses the execution of

speciﬁcations with runtime assertion checking (checking correctness of a computation for some

input) and model checking (checking correctness for all/many possible inputs).

Validating Speciﬁcations As demonstrated above, we can validate the correctness of an oper-

ation by checking whether it satisﬁes its speciﬁcation. However, it is by no means sure that the

formulas in the speciﬁcation indeed appropriately express our intentions of how the operation

shall behave: for instance, by a slight logical error, the postcondition of a speciﬁcation may

be trivially satisﬁed by every output. This kind of error can be apparently not detected by just

checking the operation.

Nevertheless RISCAL provides some means to validate the adequacy of a speciﬁcation ac-

cording to various criteria. If we press the button (Show/Hide Tasks), the user interface is

extended on the right side by a view of the folder depicted in Figure 2; this folder lists a couple

of tasks (depicted in blue) related to the currently selected operation. For instance, the task

“Execute operation” denotes the checking of the operation itself, i.e., its application to all inputs

allowed by the precondition. The execution of a task may be triggered by a double click on the

item; alternatively, by a right-click a menu pops up in which the entry “Execute Task” may be

selected. Likewise the menu entry “Print Description” prints a verbal description of the task

while “Print Deﬁnition” prints a deﬁnition of the operation to be performed.

Our focus is now on the tasks listed in the folder “Validate speciﬁcation”:

14

Figure 2: Operation-Related Tasks

Execute speciﬁcation This task executes an automatically generated function whose result is

implicitly deﬁned by the postcondition of the selected operation. For instance, in case of

the procedure gcdp, the menu entry “Print Deﬁnition” shows the following operation:

fun _gcdpSpec(m:nat, n:nat): nat

requires (m , 0) ∨ (n , 0);

= choose result:nat with result = gcd(m, n);

If we execute this task for N = 6 in non-deterministic and non-silent mode, we get the

following output which demonstrates that the postcondition indeed determines the greatest

common divisor:

Executing gcdp(Z,Z) with all 49 inputs.

Ignoring inadmissible inputs...

Run 1 of deterministic function gcdp(1,0):

Result (2 ms): 1

..

Run 17 of deterministic function gcdp(3,2):

Result (1 ms): 1

...

Run 34 of deterministic function gcdp(6,4):

Result (1 ms): 2

...

Run 48 of deterministic function gcdp(6,6):

Result (1 ms): 6

Execution completed for ALL inputs (419 ms, 48 checked, 1 inadmissible).

The execution of this task should proceed in non-deterministic mode to ensure that, if the

postcondition allows multiple outputs (which may or may be not intended, see also the

discussion concerning the last task below), all of the outputs allowed by the postcondition

15

of the operation are indeed displayed.

Is precondition satisﬁable/not trivial? These tasks demonstrate that there is at least one input

that satisﬁes the precondition respectively that there is at least one output that violates the

precondition. In more detail, the tasks denote the following theorems:

theorem _gcdpPreSat() ⇔ ∃m:nat, n:nat. ((m , 0) ∨ (n , 0));

theorem _gcdpPreNotTrivial() ⇔ ∃m:nat, n:nat. (¬((m , 0) ∨ (n , 0)));

These theorems are apparently true in our concrete case:

Executing _gcdpPreSat().

Execution completed (0 ms).

Executing _gcdpPreNotTrivial().

Execution completed (0 ms).

If the ﬁrst condition were violated, gcdp would not accept any input; if the second condition

were violated, gcdp would accept every input (both cases would make the precondition

pointless).

Is postcondition always satisﬁable? This task demonstrates that, for every input that satisﬁes

the precondition, there exists at least one output that satisﬁes the postcondition:

theorem _gcdpPostSat(m:nat, n:nat)

requires (m , 0) ∨ (n , 0);

⇔ ∃result:nat. (result = gcd(m, n));

Again, this theorem is true in our case:

Executing _gcdpPostSat(Z,Z) with all 49 inputs.

Execution completed for ALL inputs (14 ms, 48 checked, 1 inadmissible).

If the theorem were violated, the speciﬁcation could not be correctly implemented: for

some legal input, gcdp could not return any legal output.

Is postcondition always/sometimes not trivial? These tasks demonstrate that the postcondi-

tion indeed rules out some illegal outputs (otherwise the postcondition would be point-

less). In more detail, the ﬁrst (stronger) theorem states that for every input some outputs

are prohibited:

theorem _gcdpPostNotTrivialAll(m:nat, n:nat)

requires (m , 0) ∨ (n , 0);

⇔ ∃result:nat. (¬(result = gcd(m, n)));

However, sometimes an operation might indeed allow for some special cases of inputs

arbitrary outputs. Therefore we provide a second (weaker) theorem that states that at least

for some input not all outputs are allowed:

theorem _gcdpPostNotTrivialSome()

⇔ ∃m:nat, n:nat with (m , 0) ∨ (n , 0).

(∃result:nat. (¬(result = gcd(m, n))));

In our case, both theorems hold:

16

Executing gcdp(Z,Z) with all 49 inputs.

Execution completed for ALL inputs (65 ms, 48 checked, 1 inadmissible).

Executing _gcdpPostNotTrivialSome().

Execution completed (0 ms).

Is output uniquely determined? This theorem allows to detect unintentionally underspeciﬁed

operations, i.e., operations that by a logical error in the postcondition allow multiple

outputs even when this is not desired. In more detail, the corresponding theorem states

that for every legal input there exists at most one legal output:

theorem _gcdpPostUnique(m:nat, n:nat)

requires (m , 0) ∨ (n , 0);

⇔ ∀result:nat with result = gcd(m, n).

(∀_result:nat with let result = _result in (result = gcd(m, n)).

(result = _result));

In our example, this theorem indeed holds:

Executing _gcdpPostUnique(Z,Z) with all 49 inputs.

Execution completed for ALL inputs (52 ms, 48 checked, 1 inadmissible).

This theorem need not generally hold, because a function might be intentionally under-

speciﬁed such that multiple outputs are acceptable. However, if the theorem holds, the

procedure has no choice in which value it may return.

3 More Examples

We continue by presenting some more examples of RISCAL speciﬁcations.

Insertion Sort We are going to specify the Insertion Sort algorithm for sorting arrays of

length N that hold natural numbers up to size M, based on the following declarations (see

Appendix C.2 for the full speciﬁcation):

val N:Nat;

val M:Nat;

We make use of the following type deﬁnitions

type nat = Nat[M];

type array = Array[N,nat];

type index = Nat[N-1];

where type array is the type of all arrays of length N of values of type nat to be accessed by

indices 0, . . . , N − 1; type index denotes the domain of legal indices.

The insertion sort algorithm is then deﬁned as follows:

proc sort(a:array): array

ensures ∀i:nat. i < N-1 => result[i] ≤ result[i+1];

17

ensures ∃p:Array[N,index].

(∀i:index,j:index. i , j ⇒ p[i] , p[j]) ∧

(∀i:index. a[i] = result[p[i]]);

{

var b:array = a;

for var i:Nat[N]:=1; i<N; i:=i+1 do

decreases N-i;

{

var x:nat := b[i];

var j:Int[-1,N] := i-1;

while j ≥ 0 ∧ b[j] > x do

decreases j+1;

{

b[j+1] := b[j];

j := j-1;

}

b[j+1] := x;

}

return b;

}

The postcondition of this algorithm states that the resulting array is sorted in ascending order

and that that it is a permutation of the input array, i.e., that there exists a permutation p of indices

such that the result array holds at position p[i] the value of the input array at position i. The loop

is annotated with appropriate termination measures (invariants have been omitted).

The speciﬁcation demonstrates that arrays can be used in a style similar to most imperative

programming languages. Semantically, however, arrays in RISCAL diﬀer from programming

language arrays in that an array assignment a[i] := e does not update the existing array but

overwrites the program variable a with a new array that is identical to the original one except

that it holds at position i value e. RISCAL arrays thus have value semantics rather than pointer

semantics. Correspondingly, above procedure does not update the argument array a; it rather

creates a new array b that is returned as the result of the procedure (actually, because of the

semantics of the array assignment, the use of a separate variable b is not necessary; the program

could have just used a and terminated with the statement return b).

We can demonstrate a single run of the system by deﬁning the procedure

proc main(): Unit

{

choose a: array;

print a, sort(a);

}

and selecting in menu “Operation” the entry main(). Executing this speciﬁcation for N = 3 and

in “Deterministic” mode gives output

Run of deterministic function main():

18

[0,0,0,0],[0,0,0,0]

Result (6 ms): ()

Execution completed (46 ms).

Not all nondeterministic branches may have been considered.

which however only demonstrates that the array holding 0 everywhere is appropriately “sorted”.

By setting the option Nondeterministic, the output

Executing main().

Branch 0 of nondeterministic function main():

[0,0,0],[0,0,0]

Result (8 ms): ()

Branch 1 of nondeterministic function main():

[1,0,0],[0,0,1]

Result (8 ms): ()

Branch 2 of nondeterministic function main():

[2,0,0],[0,0,2]

...

Branch 255 of nondeterministic function main():

[3,3,3,3],[3,3,3,3]

Result (10 ms): ()

Branch 256 of nondeterministic function main():

No more results (5056 ms).

Execution completed (5062 ms).

demonstrates that this is the case for all other inputs as well. Setting the option Silent and

selecting the operation sort(Map[Array[Z]]), gives with the output

Executing sort(Array[Z]) with all 256 inputs.

Execution completed for ALL inputs (327 ms, 256 checked, 0 inadmissible).

Not all nondeterministic branches may have been considered.

the core information in much shorter time.

DPLL Algorithm As a somewhat bigger example, we present the core of the DPLL (Davis,

Putnam, Logemann, Loveland) algorithm for deciding the satisﬁability of propositional logic

formulas with at most n variables in conjunctive normal form. We start with the following

declaration (the full speciﬁcation is given in Appendix C.3):

val n: N;

A literal (a propositional variable in positive or negated form) is represented by a positive

respectively negative integer; a clause (a conjunction of literals) is represented by a set of literals;

a formula (a disjunction of clauses) is represented by a set of clauses. A valuation of a formula

(a mapping of propositional variables to truth values) is represented by the set of literals that are

mapped to “true”. All of this gives rise to the following type deﬁnitions:

19

type Literal = Z[-n,n];

type Clause = Set[Literal];

type Formula = Set[Clause];

type Valuation = Set[Literal];

Actually, these deﬁnitions only introduce “raw types”: not every value of this type is meaningful.

Based on the predicate

pred consistent(l:Literal,c:Clause) ⇔ ¬(l∈c ∧ -l∈c);

we introduce side conditions that all meaningful values of the corresponding types must satisfy:

pred literal(l:Literal) ⇔ l,0;

pred clause(c:Clause) ⇔ ∀l∈c. literal(l) ∧ consistent(l,c);

pred formula(f:Formula) ⇔ ∀c∈f. clause(c);

pred valuation(v:Valuation) ⇔ clause(v);

We can deﬁne the predicates that state when a valuation satisﬁes a literal, a clause, and a formula,

respectively:

pred satisfies(v:Valuation, l:Literal) ⇔ l∈v;

pred satisfies(v:Valuation, c:Clause) ⇔ ∃l∈c. satisfies(v, l);

pred satisfies(v:Valuation, f:Formula) ⇔ ∀c∈f. satisfies(v,c);

We thus deﬁne the core notion of the satisﬁability of a formula respectively, it’s counterpart,

validity:

pred satisfiable(f:Formula) ⇔

∃v:Valuation. valuation(v) ∧ satisfies(v,f);

pred valid(f:Formula) ⇔

∀v:Valuation. valuation(v) ⇒ satisfies(v,f);

We deﬁne the negation of a formula

fun not(f: Formula):Formula =

{ c | c:Clause with clause(c) ∧ ∀d ∈f. ∃l∈d. -l∈c };

theorem notFormula(f:Formula)

requires formula(f);

⇔ formula(not(f));

and deﬁne core relationship between both notions: a formula is valid, if its negation is not

satisﬁable:

theorem notValid(f:Formula)

requires formula(f);

⇔ valid(f) ⇔ ¬satisfiable(not(f));

Having established the basic theory of propositional formulas and their satisﬁability, we introduce

some auxiliary notions used by the DPLL algorithm, namely the set of all literals of a formula

20

fun literals(f:Formula):Set[Literal] =

{l | l:Literal with ∃c∈f. l∈c};

and the result of setting a literal l in formula f to “true”:

fun substitute(f:Formula,l:Literal):Formula =

{c\{-l} | c∈f with ¬(l∈c)};

We are now in the position to give the recursive version of the algorithm (omitting for brevity

the optimizations that actually make the algorithm eﬃcient):

multiple pred DPLL(f:Formula)

requires formula(f);

ensures result ⇔ satisfiable(f);

decreases |literals(f)|;

⇔

if f = ∅[Clause] then

>

else if ∅[Literal] ∈ f then

⊥

else

choose l∈literals(f) in

DPLL(substitute(f,l)) ∨ DPLL(substitute(f,-l));

The speciﬁcation of the algorithm states that for every well-formed formula f the algorithm

yields “true” if and only if f is satisﬁable. If it cannot easily decide the satisﬁability of f , the

algorithm chooses a literal in that is substituted once by “true” and once by “false” and calls

itself recursively on the resulting formulas; if one of them is satisﬁable, also f is satisﬁable.

The algorithm terminates because in every recursive invocation the number of literals in the

formula is decreased. The keyword multiple in front of the deﬁnition is necessary for recursive

functions/predicates with nondeterministic semantics, as in the case of this function that applies

the choose operator.

For asserting the termination the iterative version of the algorithm, we introduce a couple of

auxiliary notions

fun vars(f:Formula): Set[N[n]] =

{ if l>0 then l else -l | l ∈ literals(f) };

val m = 2^(n+1)-1;

fun size(f:Formula): N[m] = 2^(|vars(f)|+1)-1;

fun size(stack:Array[n+1,Formula], i:N[n+1]): N[m] =

Í

k:N[n] with k<i. size(stack[k]);

which ultimately give a measure for the complexity of the work that is still to be performed for i

formulas stored at the beginning of an array stack (see the explanations below).

The iterative version of the algorithm can then be formulated and provided with correctness

annotations as follows:

21

proc DPLL2(f:Formula): Bool

requires formula(f);

ensures result ⇔ satisfiable(f);

{

var satisfiable: Bool := ⊥;

var stack: Array[n+1,Formula] := Array[n+1,Formula](∅[Clause]);

var number: N[n+1] := 0;

stack[number] := f;

number := number+1;

while ¬satisfiable ∧ number>0 do

invariant 0 ≤ number ∧ number ≤ n+1;

invariant satisfiable(f) ⇔ satisfiable ∨

∃i:N[n+1] with i<number. satisfiable(stack[i]);

decreases if satisfiable then 0 else size(stack, number);

{

number := number-1;

var g:Formula := stack[number];

if g = ∅[Clause] then

satisfiable := >;

else if ¬ ∅[Literal]∈g then

{

choose l∈literals(g);

stack[number] := substitute(g,-l);

number := number+1;

stack[number] := substitute(g,l);

number := number+1;

}

}

return satisfiable;

}

The algorithm operates on a stack to which it initially pushes the original formula f . It then

iteratively pops the top formula g from the stack; if the formula is not trivially satisﬁable, it

chooses a literal in g that is substituted once by “true” and once by “false”; the resulting formulas

are pushed to the stack again. The algorithm terminates when the stack becomes empty ( f is

then not satisﬁable) or if the top formula g is satisﬁable (then also f is satisﬁable).

In addition to the speciﬁcation of pre- and postcondition, the algorithm is also annotated with

the core invariants from which the correctness of the algorithms can be deduced: the original

formula is satisﬁable if the variable satisﬁable is set to “true” or if any of the formulas on the

stack is satisﬁable. It terminates, because the complexity of the work which remains on the stack

(essentially the sum of the number of corresponding applications of the recursive algorithm to

these formulas) decreases.

By setting n = 3 and deﬁning

proc main0(): ()

22

{

val f = {{1,2,3},{-1,2},{-2,3},{-3}};

val r = DPLL2(f);

print f,r;

}

we can validate the correctness of the (iterative version of the) algorithm for one particular input:

Executing main0().

Run of deterministic function main0():

{{1,2,3},{-1,2},{-2,3},{-3}},false

Result (36 ms): ()

Execution completed (100 ms).

Not all nondeterministic branches may have been considered.

However, when attempting to check the algorithm for all inputs

Executing DPLL2(Set[Set[Z]]) with all (at least 2^63) inputs.

PARALLEL execution with 4 threads (output disabled).

434480 inputs (768 checked, 140278 inadmissible, 0 ignored, 293434 open)...

434480 inputs (1792 checked, 429562 inadmissible, 0 ignored, 3126 open)...

711986 inputs (2545 checked, 587520 inadmissible, 0 ignored, 121921 open)...

1217971 inputs (3583 checked, 853627 inadmissible, 0 ignored, 360761 open)...

1500591 inputs (4096 checked, 1055731 inadmissible, 0 ignored, 440764 open)...

1724104 inputs (4096 checked, 1594493 inadmissible, 0 ignored, 125515 open)...

...

we ﬁrst realize that there are extremely many (more than 2

63

) of these and second that only a

small minority of them are well-formed (most sets of sets of integers violate some of the type

constraints). Unless we have an overwhelming amount of time (a couple of thousands of years)

at our hand, we better restrict our input space. We therefore stop the execution and introduce

constants for the maximum number of literals per clause and the maximum number of clauses

per formula:

val cn: N; // e.g. 2;

val fn: N; // e.g. 20;

We then deﬁne a function that gives us all formulas with these constraints:

fun formulas(): Set[Formula] =

let

literals = { l | l:Literal with literal(l) },

clauses = { c | c ∈ Set(literals) with |c| ≤ cn ∧ clause(c) },

formulas = { f | f ∈ Set(clauses) with |f| ≤ fn ∧ formula(f) }

in formulas;

Now we deﬁne a test program

23

proc main1(): ()

{

// apply check to a specific set of formulas

check DPLL with formulas();

}

in which the command check applies the algorithm to the speciﬁc set of formulas. By multi-

threaded and distributed execution we then may check for cn = 2 and fn = 20 the selected subset

of inputs in a quite limited amount of time:

Executing main1().

Executing DPLL(Set[Set[Z]]) with selected 524288 inputs.

Executing "/software/RISCAL/etc/runssh qftquad2.risc.jku.at 4"...

Connecting to qftquad2.risc.uni-linz.ac.at:56371...

Executing "/software/RISCAL/etc/runmach 4"...

Connecting to localhost:9999...

Connected to remote servers.

PARALLEL execution with 4 local threads and 2 remote servers (output disabled).

8668 inputs (4674 checked, 0 inadmissible, 0 ignored, 3994 open)...

22126 inputs (10737 checked, 0 inadmissible, 0 ignored, 11389 open)...

...

503297 inputs (477221 checked, 0 inadmissible, 0 ignored, 26076 open)...

Execution completed for SELECTED inputs (61037 ms, 524288 checked, 0 inadmissible).

Execution completed (89457 ms).

Not all nondeterministic branches may have been considered.

As this example demonstrates, model checking experiments may have to be planned with care to

yield meaningful results with restricted (time and space) resources.

DPLL Algorithm with Subtypes As the previous example has shown, checking operations on

large domains of “raw” values from which the meaningful values have to be ﬁltered by auxiliary

preconditions can become quite cumbersome. In many cases, the use of “subtypes” may make

our lives considerably easier.

For this, we start with the following declarations that introduce the same constants as in the

previous example (the full speciﬁcation is given in Appendix C.4):

val n: N;

val cn: N;

val fn: N;

Now we deﬁne the domain of literals as follows:

type LiteralBase = Z[-n,n];

type Literal = LiteralBase with value , 0;

24

Here the type LiteralBase denotes the type of all “raw literals”; the type LiteralBase then is

deﬁned as a subtype of Literal that only includes the meaningful (non-zero) values. The clause

with value , 0 describes the side condition that every value of type Literal must fulﬁll; the

special name value denotes the value to which the condition is applied.

Correspondingly, we can introduce the other types as subtypes of raw types based on the same

auxiliary predicates that we have deﬁned in the previous example; additionally we immediately

restrict the sizes of the types such that exhaustive checking becomes feasible:

type ClauseBase = Set[Literal];

pred clause(c:ClauseBase) ⇔ ∀l∈c. ¬(l∈c ∧ -l∈c);

type Clause = ClauseBase with |value| ≤ cn ∧ clause(value);

type FormulaBase = Set[Clause];

pred formula(f:FormulaBase) ⇔ ∀c∈f. clause(c);

type Formula = FormulaBase with |value| ≤ fn ∧ formula(value);

type Valuation = ClauseBase with clause(value);

When we now process the speciﬁcation, we get the following output which shows the processing

of the subtype deﬁnitions:

Using n=3.

Using cn=2.

Using fn=20.

Evaluating the domain of Literal...

Evaluating the domain of Clause...

Evaluating the domain of Formula...

Evaluating the domain of Valuation...

Computing the value of m...

Type checking and translation completed.

Now, in the following deﬁnitions all occurrences of the side conditions can be removed, e.g.

rather than writing

fun not(f: Formula):Formula =

{ c | c:Clause with clause(c) ∧ ∀d ∈f. ∃l∈d. -l∈c };

theorem notFormula(f:Formula)

requires formula(f);

⇔ formula(not(f));

(as we did in the previous example), we can now write

fun not(f: Formula):Formula =

{ c | c:Clause with ∀d∈f. ∃l∈d. -l∈c };

theorem notFormula(f:Formula) ⇔ formula(not(f));

25

Furthermore, we can drop from predicate DPLL and procedure DPLL2 the precondition clause

requires formula(f) which is now subsumed by the deﬁnition of subtype Formula.

When now checking the algorithm for all inputs, we get the following output:

Executing DPLL2(Formula) with all 524288 inputs.

PARALLEL execution with 4 threads (output disabled).

2081 inputs (1519 checked, 0 inadmissible, 0 ignored, 562 open)...

3507 inputs (2842 checked, 0 inadmissible, 0 ignored, 665 open)...

4153 inputs (3974 checked, 0 inadmissible, 0 ignored, 179 open)...

5247 inputs (5082 checked, 0 inadmissible, 0 ignored, 165 open)...

6334 inputs (6123 checked, 0 inadmissible, 0 ignored, 211 open)...

7344 inputs (7151 checked, 0 inadmissible, 0 ignored, 193 open)...

...

Compared to the output from the previous example, we see that the domain of the check has been

automatically restricted to the values of interest.

4 Related Work

RISCAL is related to a large body of prior research; we only give a short account of the work

that seems most relevant.

Various languages arisen in the context of automated reasoning systems, while being designed

for specifying logical theories, have some executable ﬂavor: Theorema [6, 30] has been de-

signed at RISC as a system for computer supported mathematical theorem proving and theory

exploration; its PCS (Prove-Compute-Solve) paradigm considers computing as a special kind

of proving. Also a compiler for an executable subset of the Theorema language to Java was

developed. The language of the formal proof management system Coq [4, 8] allows to write

executable algorithms from which functional programs in the programming languages OCaml,

Haskell, and Scheme can be extracted; since the correctness of the algorithms can be formulated

and veriﬁed in Coq, the programs are guaranteed to be correct. Similarly, the higher order

logic HOL of the generic proof assistant Isabelle [20, 13] embeds a functional programming

language in which algorithms can be deﬁned and veriﬁed and converted to programs in OCaml,

Haskell, SML, and Scala. In [19], Isabelle is used to deﬁne the formal semantics of a simple

imperative semantics from which executable code can be generated. However, all this work is

targeted towards generating executable code from veriﬁed algorithms; it does not really address

the problem stated in Section 1 of validating the correctness of algorithms before veriﬁcation.

Also the abstract data type speciﬁcation languages of the OBJ family [12, 11] include a large

executable subset, essentially generalizations of functional programming languages. Using the

supporting rewriting engines, programs in these languages can be also model-checked. However,

the logics of these languages are based on equational logic which is much more restricted than

predicate logic by enforcing the formulation of predicates in a low-level executable style.

As for algorithm languages, SETL [29, 28] is an old very high-level programming language

based on set theory; it supports set comprehensions and quantiﬁed formulas as programming

language constructs but not formal speciﬁcations. Alloy [14, 2] is a language for describing

26

structures and their relationships, e.g., the conﬁgurations of a data structure arising from a

sequence of modifying operations. The language is based on a relational logic; the Alloy

Analyzer is a satisﬁability solver that ﬁnds structures satisfying given constraints. While Alloy

can be used to formulate algorithms/programs, this can become quite challenging [24], because

the language diﬀers very much from conventional languages. Event-B [1, 10] is a formal method

for the modeling and analysis of systems, based on set theory as a modeling notation and the

concept of reﬁnement to represent systems at diﬀerent abstraction levels; the supporting Rodin

tool embeds an interactive proving assistant for verifying the correctness of system designs and

reﬁnements. The Event-B language is more oriented towards modeling reactive systems than

conventional algorithms/programs [24].

RISCAL has been more directly inﬂuenced by the temporal logic of actions (TLA) [16, 31]

which has evolved into a speciﬁcation language TLA+ for describing concurrent systems. It

also supports a the more conventional algorithm language PlusCal by translation to TLA+

speciﬁcations; PlusCal can be used to describe iterative algorithms but does not support recursion.

TLA+/PlusCal is based on classical ﬁrst order logic and set theory and supported by the TLC

model checker and the TLA+ proof system. The RISCAL use of externally deﬁned constants to

restrict domains has been inspired by the corresponding use of constants by TLA+/PlusCal to

restrict the sizes of sets. However, while RISCAL is statically typed, TLA+/PlusCal has no static

type system; indeed all values are ultimately sets. PlusCal demonstrates its heritage from TLA+

in that it has no direct means of specifying an algorithm’s pre- or post-conditions, invariants,

and termination measures; such properties have to be expressed via assertions or via temporal

formulas that refer to the value of the program counter.

The algorithm language with probably the longest tradition is VDM [17, 21] that supports in

a typed framework with a rich set of types an expressive language for modeling both recursive

and iterative algorithms with algorithms speciﬁed in terms of pre- and post-conditions. The

supporting software Overture also provides an execution-based model checker similar to RISCAL

(while a supporting proof tool is still in its infancy). However, there are some language glitches

which make the use of the system somewhat cumbersome [24]: for instance, it is not possible to

introduce named predicates in invariants; furthermore, invariants can be only used to constrain

global state changes but not individual loops.

The language WhyML of the program veriﬁcation environment Why3 environment [5, 32],

while being a real programming language, can due its high-level also be considered as an algo-

rithm language supporting pre- and postconditions, assertions, loop invariants, and termination

measures. However, due to its actual nature as a programming language, WhyML does not

support nondeterministic constructions like TLA+/PlusCal, VDM, or RISCAL. WhyML pro-

grams can be executed via translation to the language OCaml and veriﬁed by various external

theorem provers; runtime assertion checking and model checking are not supported. Similarly

Dafny [18, 9] is a high-level programming language developed at Microsoft with built-in spec-

iﬁcation constructs. A program can be compiled to executable .NET code and veriﬁed via the

SMT solver Z3. Also Dafny does not support nondeterministic constructions, runtime assertion

checking or model checking.

Also for various more wide-spread programming languages such as C, Ada, Java, C#, exten-

sions for speciﬁcations do exist. Considering only the Java world, around the Java Modeling

Language (JML) [7, 15] an ecosystem of supporting tools have been developed, including run-

27

time assertion checkers, extended static checkers, and full-ﬂedged veriﬁers. However, all of

these tools have to struggle with the complex semantics of an “industrial” programming lan-

guage which is only partially covered by JML respectively the corresponding tools, partially also

with the complexity of JML itself. For instance, the runtime assertion checking supported by

the old “Common JML Tools” or the newer “OpenJML” toolset has to deal with the fact that

not all quantiﬁed formulas expressible in JML are easily executable such that not all parts of a

speciﬁcation are necessarily considered in checks.

The thesis [24] has compared some of the languages/tools mentioned above (notably JML,

TLA+/PlusCal, Alloy, VDM/Overture, Event-B/Rodin) and their suitability for modeling and

verifying mathematical algorithms; in a nutshell, while none was considered as ideal, the system

TLA+/PlusCal was judged as the best on for model checking (with VDM as an alternative for

recursive algorithms, which are not supported by PlusCal).

5 Future Work

The current version of the RISCAL software allows to validate the correctness of mathematical

algorithms and their formal annotations by executing respectively evaluating them on ﬁnite

subsets of the generally inﬁnite domains. Thus it can be e.g. detected that a loop invariant is

too strong, i.e., does not hold for all inputs and loop iterations. However, this is only a ﬁrst step

towards an environment for the general veriﬁcation of mathematical algorithms.

As a next step, we will develop a veriﬁcation condition generator for the speciﬁcation language.

The conditions are parameterized over the unspeciﬁed domain bounds; for concrete values of these

bounds, the conditions are decidable: they can be veriﬁed by evaluation (which is presumably

slow) and by application of SMT solvers (which can be expected to be reasonably eﬃcient). If

such concrete instances are invalid, also the general condition is invalid and a proof need not be

attempted. Thus we will also be able to detect that a loop invariant is too weak, i.e., that it does

not describe the value space of the loop variables accurately enough to prove that the invariant

holds in the post-state of the loop, even if it holds in the pre-state.

The expectation is that thus the formal annotations can be further validated to carry a subsequent

proof-based veriﬁcation of the algorithms for domains of arbitrary size. Ultimately, we will

therefore connect the RISCAL software to a computer-aided interactive proof assistant such as

the RISC ProofNavigator [26, 23] in order to perform general veriﬁcations.

References

[1] Jean-Raymond Abrial. Modeling in Event-B — System and Soft-

ware Engineering. Cambridge University Press, Cambridge, UK,

May 2010. http://www.cambridge.org/at/academic/subjects/

computer-science/programming-languages-and-applied-logic/

modeling-event-b-system-and-software-engineering?format=HB.

[2] Alloy: a Language & Tool for Relational Models, March 2016. http://alloy.mit.edu/

alloy.

28

[3] ANTLR, December 2016. http://www.antlr.org.

[4] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development

— Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin, Germany, 2016.

https://doi.org/10.1007/978-3-662-07964-5.

[5] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3:

Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on

Intermediate Veriﬁcation Languages, pages 53–64, Wrocław, Poland, August 2011.

http://proval.lri.fr/publications/boogie11final.pdf.

[6] Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, and Wolfgang

Windsteiger. Theorema 2.0: Computer-Assisted Natural-Style Mathematics. Journal

of Formalized Reasoning, 9(1):149–185, 2016. https://doi.org/10.6092/issn.

1972-5787/4568.

[7] Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions:

Advanced Speciﬁcation and Veriﬁcation with JML and ESC/Java2. In Frank S. de Boer,

Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Meth-

ods for Components and Objects: FMCO 2005, Amsterdam, The Netherlands, November

1-4, 2005, Revised Lectures, volume 4111 of Lecture Notes in Computer Science, pages

342–363, Berlin, Germany, 2006. Springer. https://doi.org/10.1007/11804192_16.

[8] The Coq Proof Assistant, January 2017. https://coq.inria.fr.

[9] Dafny: A Language and Program Veriﬁer for Functional Correctness, Jan-

uary 2017. https://www.microsoft.com/en-us/research/project/

dafny-a-language-and-program-verifier-for-functional-correctness.

[10] Event-B and the Rodin Platform, November 2015. http://www.event-b.org.

[11] Kokichi Futatsugi et al. CafeOBJ. Japan Advanced Institute of Science and Technology

(JAIST), Nomi, Japan, January 2017. https://cafeobj.org.

[12] Joseph A. Goguen and Grant Malcom, editors. Software Engineering with OBJ — Algebraic

Speciﬁcation in Action, volume 2 of Advances in Formal Methods. Springer US, New York,

NY, USA, 2000. https://doi.org/10.1007/978-1-4757-6541-0.

[13] Isabelle, November 2016. https://isabelle.in.tum.de.

[14] Daniel Jackson. Software Abstractions — Logic, Language, and Analysis. MIT Press,

Cambridge, MA, USA, revised edition, November 2011. https://mitpress.mit.edu/

books/software-abstractions.

[15] The Java Modeling Language (JML) Home Page, February 2013. http://www.jmlspecs.

org.

29

[16] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Soft-

ware Engineers. Addison-Wesley, 2002. http://research.microsoft.com/users/

lamport/tla/book.html.

[17] Peter Gorm Larsen et al. VDM-10 Language Manual. Overture Technical Report

TR-001, Overture Tool, September 2016. http://raw.github.com/overturetool/

documentation/master/documentation/VDM10LangMan/VDM10_lang_man.pdf.

[18] K. Rustan M. Leino. Dafny: An Automatic Program Veriﬁer for Functional Correct-

ness. In Logic Programming and Automated Reasoning (LPAR-16), Dakar, Senegal, April

25–May 1, 2010, volume 6355 of Lecture Notes in Computer Science, pages 348–370.

Springer, Berlin, Germany, 2010. https://www.microsoft.com/en-us/research/

wp-content/uploads/2008/12/dafny_krml203.pdf.

[19] Tobias Nipkow and Gerwin Klein. Concrete Semantics — With Isabelle/HOL. Springer,

Heidelberg, Germany, 2014. https://doi.org/10.1007/978-3-319-10542-0.

[20] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof

Assistant for Higher-Order Logic. Springer, Berlin, Germany, December 2016. https:

//isabelle.in.tum.de/dist/Isabelle2016-1/doc/tutorial.pdf.

[21] Overture Tool — Formal Modelling in VDM, January 2017. http://overturetool.org.

[22] The RISC ProgramExplorer, June 2016. https://www.risc.jku.at/research/

formal/software/ProgramExplorer.

[23] The RISC ProofNavigator, September 2011. https://www.risc.jku.at/research/

formal/software/ProofNavigator.

[24] Daniela Ritirc. Formally Modeling and Analyzing Mathematical Algorithms with Soft-

ware Speciﬁcation Languages & Tools. Master’s thesis, Research Institute for Symbolic

Computation (RISC), Johannes Kepler University, Linz, Austria, January 2016. https:

//www.risc.jku.at/publications/download/risc_5224/Master_Thesis.pdf.

[25] Kenneth Rosen. Discrete Mathematics and Its Applications. McGraw-Hill Education,

Columbus, OH, USA, 7th edition, 2012. http://highered.mheducation.com/sites/

0073383090/information_center_view0/index.html.

[26] Wolfgang Schreiner. The RISC ProofNavigator: A Proving Assistant for Program Ver-

iﬁcation in the Classroom. Formal Aspects of Computing, 21(3):277–291, March 2009.

https://doi.org/10.1007/s00165-008-0069-4 and https://www.risc.jku.at/

people/schreine/papers/fac2008.pdf.

[27] Wolfgang Schreiner. Computer-Assisted Program Reasoning Based on a Relational

Semantics of Programs. Electronic Proceedings in Theoretical Computer Science

(EPTCS), 79:124–142, February 2012. Pedro Quaresma and Ralph-Johan Back (eds),

Proceedings of the First Workshop on CTP Components for Educational Software

(THedu’11), Wrocław, Poland, July 31, 2011, https://doi.org/10.4204/EPTCS.79.8

30

and https://www.risc.jku.at/research/formal/software/ProgramExplorer/

papers/THeduPaper-2011.pdf.

[28] About SETL, January 2015. http://setl.org/setl.

[29] W. Kirk Snyder. The SETL2 Programming Language. Technical Report 490, Courant Insti-

tute of Mathematical Sciences, Computer Science Department, New York University, New

York, NY, USA, 1990. https://archive.org/details/setl2programming00snyd.

[30] The Theorema System, January 2017. https://www.risc.jku.at/research/

theorema/software.

[31] The TLA Home Page, November 2016. https://research.microsoft.com/en-us/

um/people/lamport/tla/tla.html.

[32] Why3 — Where Programs Meet Provers, January 2017. http://why3.lri.fr/.

31

A The Software System

In the following sections, we describe the software that implements the RISCAL language.

A.1 Installing the Software

The README ﬁle of the installation is included below.

------------------------------------------------------------------------------

README

Information on RISCAL.

Author: Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>

Copyright (C) 2016-, Research Institute for Symbolic Computation (RISC)

Johannes Kepler University, Linz, Austria, http://www.risc.jku.at

This program is free software: you can redistribute it and/or modify

it under the terms of the GNU General Public License as published by

the Free Software Foundation, either version 3 of the License, or

(at your option) any later version.

This program is distributed in the hope that it will be useful,

but WITHOUT ANY WARRANTY; without even the implied warranty of

MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the

GNU General Public License for more details.

You should have received a copy of the GNU General Public License

along with this program. If not, see <http://www.gnu.org/licenses/>.

------------------------------------------------------------------------------

RISC Algorithm Language (RISCAL)

--------------------------------

http://www.risc.jku.at/research/formal/software/RISCAL

This is the RISC Algorithm Language (RISCAL), a specification language and

associated software system for describing mathematical algorithms, formally

specifying their behavior based on mathematical theories, and validating the

correctness of algorithms, specifications, and theories by execution/evaluation.

This software has been developed at the Research Institute for Symbolic

Computation (RISC) of the Johannes Kepler University (JKU) in Linz, Austria. It

is freely available under the terms of the GNU General Public License, see file

COPYING. RISCAL runs on computers with x86-compatible processors supporting Java

8 and the Standard Widget Toolkit (SWT); it has been developed and tested on a

computer with the GNU/Linux operating system and a x86-64 processor. For

learning how to use the software, see the file "main.pdf" in the directory

"manual"; examples can be found in the directory "spec".

Please send bug reports to the author of this software:

Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>

http://www.risc.jku.at/home/schreine

Research Institute for Symbolic Computation (RISC)

32

Johannes Kepler University

A-4040 Linz, Austria

A Virtual Machine with RISCAL

-----------------------------

On the RISCAL web site, you can find a virtual GNU/Linux machine that has RISCAL

preinstalled. This virtual machine can be executed with the free virtualization

software VirtualBox (http://www.virtualbox.org) on any computer with an

x86-compatible processor running under Linux, MS Windows, or MacOS. You just

need to install VirtualBox, download the virtual machine, and import the virtual

machine into VirtualBox.

This may be for you the easiest option to run the software; if you choose this

option, see the web site for further instructions.

The Distribution

----------------

The distribution has the following contents:

README ... this file

COPYING ... the GNU General Public Licence Version 3

CHANGES ... the version history of the software

etc/

RISCAL ... the execution script

run* ... examples of server execution scripts

lib/

*.jar ... the Java compiled libraries

swt32/swt.jar ... the SWT library for GNU/Linux and x86-32 processors

swt64/swt.jar ... the SWT library for GNU/Linux and x86-64 processors

doc/

main.pdf ... the manual

spec/

*.txt ... sample specifications

src/

*/*.java ... the Java source code

Installation

------------

Copy the file etc/RISCAL to a directory in your PATH and adapt the variable JAVA

to point to the Java executable "java". Adapt LIB to point to the directory

"lib" of the distribution and adapt $LIB/swt64 to point to the directory with

the SWT library for your operating system and processor.

You should then be able to execute

RISCAL &

Third Party Software

--------------------

RISCAL uses the following open source programs and libraries. Most of this is

already included in the distribution, but if you want or need, you can download

the source code from the denoted locations (local copies are available on the

RISCAL web site) and compile it on your own. Many thanks to the respective

developers for making this great software freely available!

33

Java Development Kit 8 (or higher)

http://www.oracle.com/technetwork/java/javase/downloads/index.html

------------------------------------

Go to the "Downloads" section to download the JDK.

ANTLR 4.5

http://www.antlr.org

--------------------

This is a framework for constructing parsers and lexical analyzers used for

processing the programming/specification language of the RISC ProgramExplorer.

Go to the "Download" section to download the latest 4.* version of the library.

On a Debian 9 "stretch" GNU/Linux distribution, just install the package "antlr4"

by executing (as superuser) the command

apt-get install antlr4

The Eclipse Standard Widget Toolkit 4.7

http://www.eclipse.org/swt

---------------------------------------

This is a widget set for developing GUIs in Java.

Go to section "Stable" and download the version "Linux (x86/GTK2)" (if you use

a 32bit x86 processor) or "Linux (x86_64/GTK 2)" (if you use a 64bit x86

processor).

For the builtin "Help" to work properly, WebKitGTK 1.2.0 or newer must

be installed; e.g. on a Debian 9 "stretch" GNU/Linux distribution, just install

the package "libwebkitgtk-3.0-0" by executing (as superuser) the command

apt-get install libwebkitgtk-3.0-0

Tango Icon Library 0.8.90

http://tango.freedesktop.org

----------------------------

Go to the section "Base Icon Library", subsection "Download", to download

the icons used in RISCAL.

------------------------------------------------------------------------------

End of README.

------------------------------------------------------------------------------

A.2 Running the Software

The RISCAL software is intended to be used in interactive mode by executing the shell script

RISCAL &

which prints out the copyright message

RISC Algorithm Language 1.0 (March 1, 2017)

http://www.risc.jku.at/research/formal/software/RISCAL

34

(C) 2016-, Research Institute for Symbolic Computation (RISC)

This is free software distributed under the terms of the GNU GPL.

Execute "RISCAL -h" to see the available command line options.

-----------------------------------------------------------------

However, if we execute (as indicated in this message)

RISCAL -h

we get the following output which displays the following options:

RISCAL [ <options> ] [ <path> ]

<path>: path to a specification file

<options>: the following command line options

-h: print this message and exit

-s <T>: run in server mode with T threads

-nogui: do not use graphical user interface

-p: print the parsed specification

-t: print the typed specification with symbols

-v <I>: use integer <I> for all external values

-nd: nondeterministic execution is allowed

-e <F>: execute parameter-less function/procedure F

Most of these options were used in the initial development of the software and are preserved

mainly for historical reasons. The main exception is the option -s by which it is possible to

execute the software in “server mode”, e.g. as

RISCAL -s 4

which indicates that the software shall run as a server with 4 threads. It the prints a line such as

amir.risc.jku.at 41459 27pn3agrgjc5c1mcu14r4rcr8n

where the ﬁrst string represents the Internet name of the machine running the software, the second

word represents the number of the port where the server is listening for a connection request

and the last word represents a one-time password for authenticating the connection request. This

information can be used by another RISCAL process that runs in “Distributed” mode to connect

to the server process and forward computations to the server. See Appendix A.4 for more details.

A.3 The User Interface

Main Window The user interface depicted in Figure 3 is divided into two parts. The left part

mainly embeds an editor panel with the current speciﬁcation. The right part is mainly ﬁlled

by an output panel that shows the output of the system when analyzing the speciﬁcation that

is currently loaded in the editor. The top of both parts contains some interactive elements for

controlling the editor respectively the analyzer.

35