RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
description  |  members  |  activities  |  seminar  |  publications  |  software
  
search:
  
The RISC Algorithm Language (RISCAL)
Tutorial and Reference Manual
(Version 1.0.12)
Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University, Linz, Austria
Wolfgang.Schreiner@risc.jku.at
November 15, 2017
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 defining functions and predicates and stating
theorems) on which these specifications depend. The language is based on a type system that
ensures that all variable domains are finite; nevertheless the domain sizes may depend on
unspecified 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 specifications 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 Specification Language 41
B.1 Lexical and Syntactic Structure . . . . . . . . . . . . . . . . . . . . . . . . . . 42
B.2 Specifications 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 Quantified Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
B.7 ANTLR 4 Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
C Example Specifications 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 verification of computer programs is a very challenging task. If the program operates
on an unbounded domain of values, the only general verification technique is to generate,
from the text of the program and its specification, verification conditions, i.e., logical formulas
whose validity ensures the correctness of the program with respect to its specification. 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 first verification attempts are doomed
to fail: the verification conditions are often not valid due to (also subtle) deficiencies in the
program, its specification, or annotations. The main problem is then to find 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 effort
in verification is actually spent in attempts to prove invalid verification 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 verification feasible that
copes without extra program annotations and without manual proving efforts. One possibility
is to restrict the domain of a program such that it only operates on a finite 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 verification, also in educational
scenarios [27, 22], we have started the development of RISCAL (RISC Algorithm Language) as
an attempt to make program verification 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., quantified formulas as Boolean conditions and
implicit definitions of values by formulas) but only cares about the correctness of execution, not
its efficiency. The core idea behind RISCAL is to use automatic techniques to find problems in
a program, its specification, or its annotations, that may prevent a successful verification before
actually attempting to prove verification conditions; we thus aim to start a proof of verification
conditions only when we are reasonably confident that they are indeed valid.
As a first step towards this goal, RISCAL restricts in a program P all program variables and
mathematical variables to finite types where the number of values of a type T, however, may
depend on an unspecified constant n N. If we set n to some concrete value c, we get an
instance P
c
of P where all specifications and annotations can be effectively 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 find errors,
the verification of the general program P may be attempted. The current version of the RISCAL
software documented in this report thus supports model checking of finite domain instances of
programs via the runtime assertion checking of all possible executions, which is based on the
executability of all specifications 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
specification. 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 specification language. Appendix C gives the full source of the
specifications 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 specification 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 specification. The right part is mainly filled by an output panel that shows the output
of the system when analyzing the specification 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 specification file loaded into the editor, i.e.,
when the software is started, the specification 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
specification loaded and all options set to their default values).
Specifications are written as plain text files in Unicode format (UTF-8 encoding) with arbitrary
file 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 specifications 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 first 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 specification 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.
Specification Language As a first example of the specification language (which is defined
in Appendix B), we write a specification consisting of a mathematical theory of the greatest
common divisor and its computation by the Euclidean algorithm. This specification (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 definition
nat := {x N | x N}.
6
The value of N is not defined in the specification but in the RISCAL software. We may enter
this value either in the field “Default Value” in the right part of the window or we may open with
the button “Other Values” a window that allows to set different values for different constants; if
there is no entry for a specific constant, the “Default Value” is used.
The specification defines then a predicate
pred divides(m:nat,n:nat) p:nat. m·p = n;
which corresponds to the mathematical definition
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 defined by an implicit definition; 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 define some other values, e.g.
val g:nat = gcd(N,N-1);
which corresponds to the mathematical definition
g nat, g := gcd(N, N 1)
This function satisfies 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 satisfies the given precondition), the result of this procedure (denoted
by the keyword result) is indeed the greatest common divisor of m and n, as specified above
(i.e., the result satisfies 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 prefix 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 specification may contain definitions of
8
types,
constants, functions, predicates,
theorems, and
procedures
which may depend on (declared but) undefined natural number constants. Functions may be ex-
plicitly defined or implicitly specified 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 difference 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 difference 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 effect 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 finitely 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 specification is completely executable; in particular, all stated
claims (theorems and function/predicate/procedure annotations) are checkable.
9
Execution and Model Checking Whenever a specification file is loaded or saved (or when
the button is saved), the corresponding specification 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 specification 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
defined by a term, this value is determined by evaluating the term (which may contain arbitrary
computations including the application of user-defined functions). The values of constants may
be used as bounds in types; a specification is thus always processed for a specific set of values for
the global constants (if the user changes the values, the specification is automatically re-processed
before execution). In our example specification, 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 definition.
After the processing of a specification, the menu “Operation” lists all operations together with
their argument types (operations with different 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 specifi-
cation is first 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
specified in requires, ensures, invariant, and decreases have been checked by evaluating
the corresponding formulas respectively terms, thus also evaluating the implicitly defined 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 specification. 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 specified 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 definition 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 configure 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 firewall.
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) defined 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
specifications with runtime assertion checking (checking correctness of a computation for some
input) and model checking (checking correctness for all/many possible inputs).
Validating Specifications As demonstrated above, we can validate the correctness of an oper-
ation by checking whether it satisfies its specification. However, it is by no means sure that the
formulas in the specification indeed appropriately express our intentions of how the operation
shall behave: for instance, by a slight logical error, the postcondition of a specification may
be trivially satisfied 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 specification 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 Definition” prints a definition of the operation to be performed.
Our focus is now on the tasks listed in the folder “Validate specification”:
14
Figure 2: Operation-Related Tasks
Execute specification This task executes an automatically generated function whose result is
implicitly defined by the postcondition of the selected operation. For instance, in case of
the procedure gcdp, the menu entry “Print Definition” 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 satisfiable/not trivial? These tasks demonstrate that there is at least one input
that satisfies 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 first 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 satisfiable? This task demonstrates that, for every input that satisfies
the precondition, there exists at least one output that satisfies 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 specification 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 first (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 underspecified
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-
specified 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 specifications.
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 specification):
val N:Nat;
val M:Nat;
We make use of the following type definitions
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 defined 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 specification demonstrates that arrays can be used in a style similar to most imperative
programming languages. Semantically, however, arrays in RISCAL differ 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 defining the procedure
proc main(): Unit
{
choose a: array;
print a, sort(a);
}
and selecting in menu “Operation” the entry main(). Executing this specification 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 satisfiability of propositional logic
formulas with at most n variables in conjunctive normal form. We start with the following
declaration (the full specification 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 definitions:
19
type Literal = Z[-n,n];
type Clause = Set[Literal];
type Formula = Set[Clause];
type Valuation = Set[Literal];
Actually, these definitions only introduce “raw types”: not every value of this type is meaningful.
Based on the predicate
pred consistent(l:Literal,c:Clause) ¬(lc -lc);
we introduce side conditions that all meaningful values of the corresponding types must satisfy:
pred literal(l:Literal) l,0;
pred clause(c:Clause) lc. literal(l) consistent(l,c);
pred formula(f:Formula) cf. clause(c);
pred valuation(v:Valuation) clause(v);
We can define the predicates that state when a valuation satisfies a literal, a clause, and a formula,
respectively:
pred satisfies(v:Valuation, l:Literal) lv;
pred satisfies(v:Valuation, c:Clause) lc. satisfies(v, l);
pred satisfies(v:Valuation, f:Formula) cf. satisfies(v,c);
We thus define the core notion of the satisfiability of a formula respectively, its 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 define the negation of a formula
fun not(f: Formula):Formula =
{ c | c:Clause with clause(c) d f. ld. -lc };
theorem notFormula(f:Formula)
requires formula(f);
formula(not(f));
and define core relationship between both notions: a formula is valid, if its negation is not
satisfiable:
theorem notValid(f:Formula)
requires formula(f);
valid(f) ¬satisfiable(not(f));
Having established the basic theory of propositional formulas and their satisfiability, 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 cf. lc};
and the result of setting a literal l in formula f to “true”:
fun substitute(f:Formula,l:Literal):Formula =
{c\{-l} | cf with ¬(lc)};
We are now in the position to give the recursive version of the algorithm (omitting for brevity
the optimizations that actually make the algorithm efficient):
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 lliterals(f) in
DPLL(substitute(f,l)) DPLL(substitute(f,-l));
The specification of the algorithm states that for every well-formed formula f the algorithm
yields “true” if and only if f is satisfiable. If it cannot easily decide the satisfiability 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 satisfiable, also f is satisfiable.
The algorithm terminates because in every recursive invocation the number of literals in the
formula is decreased. The keyword multiple in front of the definition 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 lliterals(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 satisfiable, 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 satisfiable) or if the top formula g is satisfiable (then also f is satisfiable).
In addition to the specification 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 satisfiable if the variable satisfiable is set to “true” or if any of the formulas on the
stack is satisfiable. 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 defining
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 first 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 define 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 define 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 specific 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 filtered 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 specification is given in Appendix C.4):
val n: N;
val cn: N;
val fn: N;
Now we define 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
defined 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 fulfill; 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 defined 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) lc. ¬(lc -lc);
type Clause = ClauseBase with |value| cn clause(value);
type FormulaBase = Set[Clause];
pred formula(f:FormulaBase) cf. clause(c);
type Formula = FormulaBase with |value| fn formula(value);
type Valuation = ClauseBase with clause(value);
When we now process the specification, we get the following output which shows the processing
of the subtype definitions:
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 definitions 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. ld. -lc };
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 df. ld. -lc };
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 definition 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 flavor: 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 verified 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 defined and verified and converted to programs in OCaml,
Haskell, SML, and Scala. In [19], Isabelle is used to define 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 verified algorithms; it does not really address
the problem stated in Section 1 of validating the correctness of algorithms before verification.
Also the abstract data type specification 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 quantified formulas as programming
language constructs but not formal specifications. Alloy [14, 2] is a language for describing
26
structures and their relationships, e.g., the configurations of a data structure arising from a
sequence of modifying operations. The language is based on a relational logic; the Alloy
Analyzer is a satisfiability solver that finds structures satisfying given constraints. While Alloy
can be used to formulate algorithms/programs, this can become quite challenging [24], because
the language differs 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 refinement to represent systems at different abstraction levels; the supporting Rodin
tool embeds an interactive proving assistant for verifying the correctness of system designs and
refinements. The Event-B language is more oriented towards modeling reactive systems than
conventional algorithms/programs [24].
RISCAL has been more directly influenced by the temporal logic of actions (TLA) [16, 31]
which has evolved into a specification language TLA+ for describing concurrent systems. It
also supports a the more conventional algorithm language PlusCal by translation to TLA+
specifications; PlusCal can be used to describe iterative algorithms but does not support recursion.
TLA+/PlusCal is based on classical first order logic and set theory and supported by the TLC
model checker and the TLA+ proof system. The RISCAL use of externally defined 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 specified 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 verification 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 verified 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-
ification constructs. A program can be compiled to executable .NET code and verified 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 specifications 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-fledged verifiers. 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 quantified formulas expressible in JML are easily executable such that not all parts of a
specification 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 finite
subsets of the generally infinite 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 first step
towards an environment for the general verification of mathematical algorithms.
As a next step, we will develop a verification condition generator for the specification language.
The conditions are parameterized over the unspecified domain bounds; for concrete values of these
bounds, the conditions are decidable: they can be verified by evaluation (which is presumably
slow) and by application of SMT solvers (which can be expected to be reasonably efficient). 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 verification 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 verifications.
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 Verification 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 Specification and Verification 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 Verifier 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
Specification 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 Verifier 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 Specification Languages & Tools. Masters 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-
ification 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 file 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 first 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 specification. The right part is mainly filled
by an output panel that shows the output of the system when analyzing the specification that
is currently loaded in the editor. The top of both parts contains some interactive elements for
controlling the editor respectively the analyzer.
35