RISC RISC Research Institute for Symbolic Computation  
The RISC Algorithm Language (RISCAL)
Tutorial and Reference Manual
(Version 2.1.*)
Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University, Linz, Austria
Wolfgang.Schreiner@risc.jku.at
August 14, 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 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, we determine
a finite model in which all algorithms, functions, and predicates are executable, and all
formulas are 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. Furthermore,
a verification condition generator allows to validate, by generating verification conditions
and checking them in some model, whether the program annotations are strong enough to
subsequently perform a proof-based verification that ensures the general correctness of the
algorithm for infinitely many models.
1
Contents
1 Introduction 4
2 A Quick Start 5
2.1 System Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Specification Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.3 Language Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.4 Execution and Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.5 Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.6 Validating Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.7 Verifying Implementations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.8 Visualizing Execution Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.9 Visualizing Evaluation Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3 More Examples 37
3.1 Linear and Binary Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.2 Insertion Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.3 DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.4 DPLL Algorithm with Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . 51
4 Related Work 53
5 Conclusions and Future Work 56
A The Software System 61
A.1 Installing the Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
A.2 Running the Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
A.3 The User Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
A.4 Distributed Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
A.5 Visualization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
B The Specification Language 73
B.1 Lexical and Syntactic Structure . . . . . . . . . . . . . . . . . . . . . . . . . . 73
B.2 Specifications and Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . 76
B.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
B.2.2 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
B.2.3 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
B.3 Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
B.3.1 Declarations and Assignments . . . . . . . . . . . . . . . . . . . . . . 81
B.3.2 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
B.3.3 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
B.3.4 Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
B.3.5 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
B.4 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
2
B.5 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
B.5.1 Constants and Applications . . . . . . . . . . . . . . . . . . . . . . . . 88
B.5.2 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
B.5.3 Equalities and Inequalities . . . . . . . . . . . . . . . . . . . . . . . . 89
B.5.4 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
B.5.5 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
B.5.6 Tuples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
B.5.7 Records . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
B.5.8 Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
B.5.9 Maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
B.5.10 Recursive Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
B.5.11 Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
B.5.12 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
B.5.13 Binders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
B.5.14 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
B.5.15 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
B.6 Quantified Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
B.7 ANTLR 4 Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
C Example Specifications 104
C.1 Euclidean Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
C.2 Bubble Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
C.3 Linear and Binary Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
C.4 Insertion Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
C.5 DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
C.6 DPLL Algorithm with Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . 112
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 [31, 25], 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 [28]. 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 . 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
4
program 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. Thus since Version 1
the RISCAL software has supported 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).
However, ensuring the correctness of formal annotations such as loop invariants by model
checking program executions only ensures that the annotations are not too strong, i.e., that
they are not violated by any execution. Checking program executions does not rule out that
the annotations are too weak to derive from them valid verification conditions that ensure the
correctness of the program by a proof-based verification (which is required, if the general
correctness of the program for models of arbitrary size is to be ensured); in particular, a loop
invariant may not be inductive, i.e., it may be to week to ensure its preservation across loop
iterations. Therefore Version 2 of the RISCAL software documented in this report also includes
a verification condition generator that produces from the annotations verification conditions
whose validity ensures the correctness of the program; since these conditions are formulas, they
may be also checked in a finite model by the RISCAL model checker. A successful check of these
conditions demonstrates that with these annotations a proof-based verification in that model is
possible; this increases our confidence that with these annotations also a proof-based verification
for models of arbitrary size may succeed (conversely, if the check fails, this demonstrates that
such a proof-based verification need not be attempted yet).
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. Further examples
on the use of this software is provided by some publications that may be also downloaded from
this web site, e.g. [32].
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 19 on page 66).
2.1 System Overview
The system is started from the command line by executing
5
Figure 1: The RISCAL User Interface
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
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
6
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.
2.2 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: ;
type nat = [N];
that introduce a natural number constant N a type nat that consists of the values 0, . . . , N (the
symbol may be entered as Nat followed by pressing the keys <Ctrl>-#) which corresponds
to the mathematical definition
nat := {x | x N}.
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.
7
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:
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 a , 0 b , 0;
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 clauses state the crucial property
for proving the correctness of the algorithm: before and after every iteration of the loop, the
8
greatest common divisor of the current values of program variables a and b (of which at least one
is not zero) 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. Furthermore, RISCAL generates from these clauses verification conditions whose
validity implies the correctness of the program with respect to its specification (see Section 2.7).
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.
2.3 Language Features
As shown above, a RISCAL specification may contain definitions of
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
9
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.
2.4 Execution and Model Checking
Whenever a specification file is loaded or saved, the corresponding specification is processed,
i.e., checked for syntactic and type errors (with graphical markers indicating 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 these values, the specification
is automatically re-processed before execution). In our example, we may thus get 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)
10
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).
WARNING: not all nondeterministic branches have been considered.
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): ()
...
11
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.
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.
12
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(,), which yields the following execution:
Executing gcdp(,) 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).
WARNING: not all nondeterministic branches 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
Executing gcdp(,) with all 16 inputs.
Execution completed for ALL inputs (6 ms, 15 checked, 1 inadmissible).
WARNING: not all nondeterministic branches have been considered.
which just gives the essential information.
2.5 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(,) 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)...
13
Execution completed for ALL inputs (8826 ms, 3720 checked, 1 inadmissible).
WARNING: not all nondeterministic branches 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(,) 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)...
8716 inputs (7408 checked, 1 inadmissible, 0 ignored, 1307 open)...
Execution completed for ALL inputs (18500 ms, 10200 checked, 1 inadmissible).
WARNING: not all nondeterministic branches 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(,) 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(,) with all 10201 inputs.
PARALLEL execution with 4 threads (output disabled).
1904 inputs (1704 checked, 0 inadmissible, 0 ignored, 200 open)...
14
Figure 2: Operation-Related Tasks
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).
WARNING: not all nondeterministic branches have been considered.
validates its correctness.
As illustrated by these examples, the RISCAL software encompasses the execution of specifi-
cations with runtime assertion checking (checking correctness of a computation for some input)
and model checking (checking correctness for all/many possible inputs).
2.6 Validating Specifications
As demonstrated above, we can validate the correctness of an operation 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 the left part of Figure 2; this folder
lists a couple of tasks related to the currently selected operation. These tasks are initially colored
red (and marked with a cloud symbol) to indicate that they are still open; once they have been
performed, they become blue (and are marked with a sun symbol) as shown in the right part of
Figure 2. Our focus is now on the tasks generated for the greatest common divisor function gcdp
introduced in Section 2.2 and checked in Section 2.4.
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
15
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 its definition
(i.e. the definition of an executable operation in the RISCAL language).
Furthermore, the folder “Validate specification” lists the following 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(,) 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
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:
16
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(,) 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:
Executing gcdp(,) with all 49 inputs.
Execution completed for ALL inputs (65 ms, 48 checked, 1 inadmissible).
Executing _gcdpPostNotTrivialSome().
Execution completed (0 ms).
17