The RISC Algorithm Language (RISCAL)

Tutorial and Reference Manual

(Version 2.7.*)

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC)

Johannes Kepler University, Linz, Austria

Wolfgang.Schreiner@risc.jku.at

March 11, 2019

Abstract

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

and associated software system for describing (potentially nondeterministic) mathematical

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

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

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

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

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

unspeciﬁed numerical constants. By instantiating these constants with values, we determine

a ﬁnite 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 speciﬁcations for all possible input values of the parameter domains. Furthermore,

a veriﬁcation condition generator allows to validate, by generating veriﬁcation conditions

and checking them in some model, whether the program annotations are strong enough to

subsequently perform a proof-based veriﬁcation that ensures the general correctness of the

algorithm for inﬁnitely many models.

1

Contents

1 Introduction 4

2 A Quick Start 5

2.1 System Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2.2 Speciﬁcation Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.3 Language Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.4 Execution and Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.5 Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2.6 Validating Speciﬁcations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

A.3 The User Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

A.4 Distributed Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

A.5 Visualization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

B The Speciﬁcation Language 75

B.1 Lexical and Syntactic Structure . . . . . . . . . . . . . . . . . . . . . . . . . . 75

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

B.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78

B.2.2 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79

B.2.3 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80

B.3 Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83

B.3.1 Declarations and Assignments . . . . . . . . . . . . . . . . . . . . . . 83

B.3.2 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84

B.3.3 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84

B.3.4 Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

B.3.5 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87

B.4 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

2

B.5 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

B.5.1 Constants and Applications . . . . . . . . . . . . . . . . . . . . . . . . 90

B.5.2 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

B.5.3 Equalities and Inequalities . . . . . . . . . . . . . . . . . . . . . . . . 91

B.5.4 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

B.5.5 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

B.5.6 Tuples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

B.5.7 Records . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

B.5.8 Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

B.5.9 Maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

B.5.10 Recursive Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96

B.5.11 Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

B.5.12 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

B.5.13 Binders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98

B.5.14 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98

B.5.15 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99

B.6 Quantiﬁed Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

B.7 ANTLR 4 Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

C Example Speciﬁcations 107

C.1 Euclidean Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107

C.2 Bubble Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108

C.3 Linear and Binary Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109

C.4 Insertion Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110

C.5 DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112

C.6 DPLL Algorithm with Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . 115

3

1 Introduction

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

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

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

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

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

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

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

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

to construct successful proofs.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

operating on unbounded domains with executions of unbounded length.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance P

c

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

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

4

program and check the annotations for all possible inputs (model checking); only if we do not

ﬁnd errors, the veriﬁcation of the general program P may be attempted. Thus since Version 1

the RISCAL software has supported model checking of ﬁnite domain instances of programs via

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

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

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 veriﬁcation conditions that ensure the

correctness of the program by a proof-based veriﬁcation (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 veriﬁcation condition generator that produces from the annotations veriﬁcation conditions

whose validity ensures the correctness of the program; since these conditions are formulas, they

may be also checked in a ﬁnite model by the RISCAL model checker. A successful check of these

conditions demonstrates that with these annotations a proof-based veriﬁcation in that model is

possible; this increases our conﬁdence that with these annotations also a proof-based veriﬁcation

for models of arbitrary size may succeed (conversely, if the check fails, this demonstrates that

such a proof-based veriﬁcation 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

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

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

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

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

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

2 A Quick Start

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

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

Figure 19 on page 67).

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 speciﬁcation. The right part is mainly ﬁlled by an output panel that shows the output

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

6

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

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

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

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

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

2.2 Speciﬁcation Language

As a ﬁrst example of the speciﬁcation language (which is deﬁned in Appendix B), we write

a speciﬁcation consisting of a mathematical theory of the greatest common divisor and its

computation by the Euclidean algorithm. This speciﬁcation (whose full content is given in

Appendix C.1) starts with the declarations

val N: ;

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 deﬁnition

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

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

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

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

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

The speciﬁcation deﬁnes then a predicate

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

which corresponds to the mathematical deﬁnition

divides ⊆ nat × nat

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

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

We then introduce the “greatest common divisor” function as

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

requires m , 0 ∨ n , 0;

= choose result:nat with

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

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

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

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

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

7

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

which corresponds to the mathematical deﬁnition

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

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

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

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

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

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

for all possible applications, corresponding to the mathematical propositions

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

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

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

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

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

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 satisﬁes the given precondition), the result of this procedure (denoted by

the keyword result) is indeed the greatest common divisor of m and n, as speciﬁed above (i.e.,

the result satisﬁes the given postcondition). The invariant 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

preﬁx old_), i.e., the greatest divisor of m and n. The clause decreases states the crucial

property for the termination of the algorithm: the value a + b decreases by every loop iteration

but does not become negative. While all these loop annotations are not necessary for executing

the algorithm, they formally express additional knowledge that aid our understanding of the

algorithm. Furthermore, RISCAL generates from these clauses veriﬁcation conditions whose

validity implies the correctness of the program with respect to its speciﬁcation (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 speciﬁcation may contain deﬁnitions of

• types,

• constants, functions, predicates,

• theorems, and

• procedures

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

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

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

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

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

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

function with that result type.

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

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

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

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

9

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

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

The RISCAL language has been designed in such a way that

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

• every language construct is executable, and thus

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

For instance, the truth value of a formula like

∃p:nat. m·p = n

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

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

the function

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

requires m , 0 ∨ n , 0;

= choose result:nat with ...

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

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

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

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

are executable.

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

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

2.4 Execution and Model Checking

Whenever a speciﬁcation ﬁle is loaded or saved, the corresponding speciﬁcation 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 speciﬁcation is determined: if a natural

number constant c is just declared, the value of c is taken from the user interface, either from the

panel “Other Values”or (if this panel does not list a value for c) from the box “Default Value”. If

the value of a constant is deﬁned by a term, this value is determined by evaluating the term (which

may contain arbitrary computations including the application of user-deﬁned functions). The

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

a speciﬁc set of values for the global constants (if the user changes these values, the speciﬁcation

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 deﬁnition.

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

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

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

proc main(): ()

{

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

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

}

By pressing the button

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

suming that option Nondeterminism has not been selected) the output

Executing main().

Run of deterministic function main():

0,1,1

Result (34 ms): ()

Execution completed (96 ms).

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 speciﬁ-

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

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (11 ms): ()

Branch 1 of nondeterministic function main():

0,2,2

Result (24 ms): ()

Branch 2 of nondeterministic function main():

0,3,3

Result (11 ms): ()

...

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

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

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

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

ensures result = 1;

yields output

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (6 ms): ()

Branch 1 of nondeterministic function main():

ERROR in execution of main(): evaluation of

ensures result = 1;

at line 24 in file gcd.txt:

postcondition is violated

ERROR encountered in execution.

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

setting the termination measure to

decreases a;

produces the output

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (10 ms): ()

...

Branch 4 of nondeterministic function main():

ERROR in execution of main(): evaluation of

decreases a;

at line 30 in file gcd.txt:

variant value 1 is not less than old value 1

ERROR encountered in execution.

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 speciﬁed precondition

requires m,0 ∨ n,0;

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

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

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

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

the deﬁnition of gcd.

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

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 conﬁgure the

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

output for N = 100 may then look as follows:

Executing gcdp(,) 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 ﬁrewall.

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

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

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

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

for which the output

Executing gcd2(,) 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 speciﬁ-

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 Speciﬁcations

As demonstrated above, we can validate the correctness of an operation by checking whether it

satisﬁes its speciﬁcation. However, it is by no means sure that the formulas in the speciﬁcation

indeed appropriately express our intentions of how the operation shall behave: for instance, by a

slight logical error, the postcondition of a speciﬁcation may be trivially satisﬁed by every output.

This kind of error can be apparently not detected by just checking the operation.

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

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

extended on the right side by a view of the folder depicted in 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 (by a right-click on a folder, a

corresponding button “Execute All Tasks” is displayed that executes all tasks in the folder and

in its subfolders). Likewise the menu entry “Print Description” prints a verbal description of the

task while “Print Deﬁnition” prints its deﬁnition (i.e. the deﬁnition of an executable operation

in the RISCAL language).

Furthermore, the folder “Validate speciﬁcation” lists the following tasks:

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

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

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

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

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

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

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

following output which demonstrates that the postcondition indeed determines the greatest

common divisor:

Executing gcdp(,) 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 satisﬁable/not trivial? These tasks demonstrate that there is at least one input

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

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

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 ﬁrst condition were violated, gcdp would not accept any input; if the second condition

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

pointless).

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

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

theorem _gcdpPostSat(m:nat, n:nat)

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

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

Again, this theorem is true in our case:

Executing _gcdpPostSat(,) with all 49 inputs.

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

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

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

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

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

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

are prohibited:

theorem _gcdpPostNotTrivialAll(m:nat, n:nat)

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

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

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

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

for some input not all outputs are allowed:

theorem _gcdpPostNotTrivialSome()

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

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

In our case, both theorems hold:

Executing gcdp(,) with all 49 inputs.

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

Executing _gcdpPostNotTrivialSome().

Execution completed (0 ms).

17