The RISC Algorithm Language (RISCAL)

Tutorial and Reference Manual

(Version 1.0.17)

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC)

Johannes Kepler University, Linz, Austria

Wolfgang.Schreiner@risc.jku.at

April 30, 2018

Abstract

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

and associated software system for describing (potentially nondeterministic) mathematical

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

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

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

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

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

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

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

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

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

input values of the parameter domains.

1

Contents

1 Introduction 4

2 A Quick Start 6

2.1 System Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2.2 Speciﬁcation Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

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

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

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

2.6 Validating Speciﬁcations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

2.7 Visualization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3 More Examples 21

3.1 Insertion Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

3.2 DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

3.3 DPLL Algorithm with Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . 28

4 Related Work 30

5 Future Work 32

A The Software System 35

A.1 Installing the Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

A.2 Running the Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

A.3 The User Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

A.4 Distributed Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

A.5 Visualization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

B The Speciﬁcation Language 46

B.1 Lexical and Syntactic Structure . . . . . . . . . . . . . . . . . . . . . . . . . . 46

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

B.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

B.2.2 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

B.2.3 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

B.3 Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

B.3.1 Declarations and Assignments . . . . . . . . . . . . . . . . . . . . . . 53

B.3.2 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

B.3.3 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

B.3.4 Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

B.3.5 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

B.4 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

B.5 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

B.5.1 Constants and Applications . . . . . . . . . . . . . . . . . . . . . . . . 60

B.5.2 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

2

B.5.3 Equalities and Inequalities . . . . . . . . . . . . . . . . . . . . . . . . 61

B.5.4 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

B.5.5 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

B.5.6 Tuples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

B.5.7 Records . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

B.5.8 Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

B.5.9 Maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

B.5.10 Recursive Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

B.5.11 Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

B.5.12 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

B.5.13 Binders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

B.5.14 Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

B.5.15 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68

B.6 Quantiﬁed Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68

B.7 ANTLR 4 Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69

C Example Speciﬁcations 75

C.1 Euclidean Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

C.2 Bubble Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

C.3 Insertion Sort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

C.4 DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

C.5 DPLL Algorithm with Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . 80

3

1 Introduction

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

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

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

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

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

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

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

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

to construct successful proofs.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

operating on unbounded domains with executions of unbounded length.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance P

c

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

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

4

Figure 1: The RISCAL User Interface

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

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

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

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

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

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

License, Version 3 at

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

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

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

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

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

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

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

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

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

5

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 4 on page 40).

2.1 System Overview

The system is started from the command line by executing

RISCAL &

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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: N;

type nat = N[N];

6

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

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

to the mathematical deﬁnition

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

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

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

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

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

The speciﬁcation deﬁnes then a predicate

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

which corresponds to the mathematical deﬁnition

divides ⊆ nat × nat

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

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

We then introduce the “greatest common divisor” function as

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

requires m , 0 ∨ n , 0;

= choose result:nat with

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

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

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

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

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

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

which corresponds to the mathematical deﬁnition

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

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

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

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

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

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

for all possible applications, corresponding to the mathematical propositions

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

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

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

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

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

7

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

requires m , 0 ∨ n , 0;

ensures result = gcd(m,n);

{

var a:nat := m;

var b:nat := n;

while a > 0 ∧ b > 0 do

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

decreases a+b;

{

if a > b then

a := a%b;

else

b := b%a;

}

return if a = 0 then b else a;

}

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

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

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

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

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

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

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

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

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

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

knowledge that aid our understanding of the algorithm.

Above procedure demonstrates that RISCAL incorporates an algorithmic language with the

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

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

proc main(): ()

{

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

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

}

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

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

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

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

8

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

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

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

The RISCAL language has been designed in such a way that

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

• every language construct is executable, and thus

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

For instance, the truth value of a formula like

∃p:nat. m·p = n

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

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

the function

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

requires m , 0 ∨ n , 0;

= choose result:nat with ...

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

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

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

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

are executable.

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

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

9

2.4 Execution and Model Checking

Whenever a speciﬁcation ﬁle is loaded or saved (or when the button is saved), the corresponding

speciﬁcation is processed,i.e., checked for syntactic and type errors (with graphical markers

displaying the locations of the errors) and translated into an executable representation. For this

purpose, the value of every constant introduced by a val clause on the top level of a speciﬁcation

is determined: if a natural number constant c is just declared, the value of c is taken from the user

interface, either from the panel “Other Values”or (if this panel does not list a value for c) from

the box “Default Value”. If the value of a constant is deﬁned by a term, this value is determined

by evaluating the term (which may contain arbitrary computations including the application of

user-deﬁned functions). The values of constants may be used as bounds in types; a speciﬁcation

is thus always processed for a speciﬁc set of values for the global constants (if the user changes

the values, the speciﬁcation is automatically re-processed before execution). In our example

speciﬁcation, we may thus get the output

RISC Algorithm Language 1.0 (March 1, 2017)

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

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

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

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

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

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

Using N=3.

Computing the value of g...

Type checking and translation completed.

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

computed by evaluating the deﬁnition.

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

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

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

proc main(): ()

{

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

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

}

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

suming that option Nondeterminism has not been selected) the output

Executing main().

Run of deterministic function main():

0,1,1

Result (34 ms): ()

Execution completed (96 ms).

Not all nondeterministic branches may have been considered.

10

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

divisor 1.

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

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

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (11 ms): ()

Branch 1 of nondeterministic function main():

0,2,2

Result (24 ms): ()

Branch 2 of nondeterministic function main():

0,3,3

Result (11 ms): ()

...

Branch 13 of nondeterministic function main():

3,2,1

Result (8 ms): ()

Branch 14 of nondeterministic function main():

3,3,3

Result (8 ms): ()

Branch 15 of nondeterministic function main():

No more results (434 ms).

Execution completed (441 ms).

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

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

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

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

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

ensures result = 1;

yields output

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (6 ms): ()

Branch 1 of nondeterministic function main():

ERROR in execution of main(): evaluation of

ensures result = 1;

at line 24 in file gcd.txt:

postcondition is violated

ERROR encountered in execution.

11

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

setting the termination measure to

decreases a;

produces the output

Executing main().

Branch 0 of nondeterministic function main():

0,1,1

Result (10 ms): ()

...

Branch 4 of nondeterministic function main():

ERROR in execution of main(): evaluation of

decreases a;

at line 30 in file gcd.txt:

variant value 1 is not less than old value 1

ERROR encountered in execution.

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

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

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

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

Ignoring inadmissible inputs...

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

Result (1 ms): 1

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

Result (0 ms): 2

...

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

Result (1 ms): 3

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

Not all nondeterministic branches may have been considered.

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

the speciﬁed precondition

requires m,0 ∨ n,0;

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

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

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

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

the deﬁnition of gcd.

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

12

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

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

Not all nondeterministic branches may have been considered.

which just gives the essential information.

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(Z,Z) with all 3721 inputs.

PARALLEL execution with 4 threads (output disabled).

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

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

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

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

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

Not all nondeterministic branches may have been considered.

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

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

button (Stop Execution).

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

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

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

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

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

output for N = 100 may then look as follows:

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

Executing "/software/RISCAL/etc/runssh

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

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

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

Connecting to localhost:9999...

Connected to remote servers.

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

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

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

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

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

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

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

13

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

Not all nondeterministic branches may have been considered.

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

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

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

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

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

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

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

for which the output

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

PARALLEL execution with 4 threads (output disabled).

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

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

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

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

Not all nondeterministic branches may have been considered.

validates its correctness.

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

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

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

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 Figure 2; this folder lists a couple

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

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

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

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

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

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

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

14

Figure 2: Operation-Related Tasks

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

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

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

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

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

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

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

following output which demonstrates that the postcondition indeed determines the greatest

common divisor:

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

Ignoring inadmissible inputs...

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

Result (2 ms): 1

..

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

Result (1 ms): 1

...

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

Result (1 ms): 2

...

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

Result (1 ms): 6

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

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

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

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

15

of the operation are indeed displayed.

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

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

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

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

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

These theorems are apparently true in our concrete case:

Executing _gcdpPreSat().

Execution completed (0 ms).

Executing _gcdpPreNotTrivial().

Execution completed (0 ms).

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

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

pointless).

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

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

theorem _gcdpPostSat(m:nat, n:nat)

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

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

Again, this theorem is true in our case:

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

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

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

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

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

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

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

are prohibited:

theorem _gcdpPostNotTrivialAll(m:nat, n:nat)

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

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

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

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

for some input not all outputs are allowed:

theorem _gcdpPostNotTrivialSome()

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

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

In our case, both theorems hold:

16

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

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

Executing _gcdpPostNotTrivialSome().

Execution completed (0 ms).

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

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

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

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

theorem _gcdpPostUnique(m:nat, n:nat)

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

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

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

(result = _result));

In our example, this theorem indeed holds:

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

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

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

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

procedure has no choice in which value it may return.

2.7 Visualization

If RISCAL is started and trace visualization is enabled (see Section A.5), the graphical user

interface depicts a check box “Trace”. If this option is selected, every run/check of a RISCAL

operation (procedure, function, predicate, theorem) opens a window in which an execution trace

of this operation is displayed provided that

• the option “Nondeterminism” is not selected,

• the options “Multi-Threaded” and “Distributed” are not selected.

In other words, visualization is restricted to deterministic execution of RISCAL operations in the

sequential mode of the RISCAL software.

Furthermore, the visualization essentially only displays the changes of variables by the com-

mands in the body of a procedure; for functions (including predicates and theorems) whose result

is determined by the evaluation of an expression the computation of the result is displayed as a

single step (except that also calls of other operations are displayed). The visualization is thus

currently mainly useful for understanding the operational behavior of a procedure.

We demonstrate this by a visualization of the following RISCAL model:

val N:N; val M:N;

type index = Z[-N,N];

type elem = Z[-M,M];

17

type array = Array[N, elem];

proc cswap(a:array, i:index, j:index): array

{

var b:array = a;

if b[i] > b[j] then

{

var x:elem := b[i];

b[i] := b[j];

b[j] := x;

}

return b;

}

proc bubbleSort(a:array): array

{

var b:array = a;

for var i:index := 0; i < N-1; i := i+1 do

{

for var j:index := 0; j < N-i-1; j := j+1 do

b := cswap(b,j,j+1);

}

return b;

}

This model implements a version of the “Bubble sort” algorithm as a procedure bubbleSort

that uses an auxiliary procedure cswap for the conditional swap of two array elements.

If we select the operation bubbleSort and set with the button “Other Values” the parameters

N and M to 4 and 3, respectively, the ﬁrst check of the procedure is performed with the argument

array a = [−3, −3, −3, −3]. Since here actually no swap is performed, we close the window that

pops up immediately (by clicking on the top-right button in the window frame). This lets the

execution proceed to the second check with a = [−2, −3, −3, −3] whose execution is displayed

by another window; it is this window that is shown on the top of Figure 3.

The window displays in the title the operation invocation bubbleSort([-2,-3,-3,-3])

whose execution is visualized; the tag “Level 0” indicates that this is the top-level of the execution

(every entry into the visualization of a nested procedure call increases this level by one). In the

window, we see a directed graph (a linear sequence of nodes) that are connected by directed

edges (arrows) and that are laid out in a two-dimensional manner from left to right and top to

bottom. This graph has three kinds of nodes:

• Numbered nodes represent the sequence of states constructed by performing assignments

to the variables of the procedure; such a node is always the target of a solid arrow (see

below). By hovering with the mouse pointer over such a node, a small window pops up

that displays the values of the various variables in that state (see the node numbered 17 in

the ﬁgure).

• Empty nodes represent “intermediate” states that have the same variable values as the

previous state; such a node is always the target of a dashed arrow (see below). An empty

18

Figure 3: Bubble Sort and Conditional Swap

19

node is displayed separately, because it indicates an event that helps to understand how the

state indicated by the next numbered node has been computed (see the explanation of the

dashed arrows below).

• Call nodes display a small window with a graph symbol; such a node represents the call

of another operation, the header of this window displays the call itself. A graph node is

always the target of a dashed arrow (see the explanations below).

Nodes may be selected by a mouse click and moved to another location in the display.

Nodes are connected by two types of arrows:

• Solid arrows (which lead to a numbered node) represent changes from one state to another

by the modiﬁcation of a variable (thus generally some variable value in the target node

is diﬀerent from the value of the corresponding variable in the source node). The label

associated to the arrow displays the name of the command that is responsible for the change

and in the second line (within parentheses) the new value of the variable. State changing

commands are variable assignments but also various kinds of choose statements that

nondeterministically set variables to values satisfying given conditions.

• Dashed arrows (which lead to an empty node) represent events within the change from one

state to the next that contribute to the change but do not change the state themselves. We

consider as such events on the one hand the testing of boolean conditions (respectively the

matching of recursive structures against patterns) that direct the control ﬂow of statements

(conditionals and loops) and on the other hand the application of an operation (procedure

or function) whose execution yields a value. The label associated to the arrow displays the

test expression respectively the application expression in the ﬁrst line and the result of the

test respectively of the application (within parentheses) in the second line.

The labels associated to the arrows (actually to the source nodes of the arrows) may be selected

by a mouse click and moved to another location in the display. In fact, some of the arrow labels

displayed in the ﬁgure have been manually moved for greater clarity.

By double-clicking on a call node which represents the application of an operation the content

of the window is modiﬁed to visualize the execution of that operation. The left diagram at the

bottom of Figure 3 displays the execution corresponding to one application of cswap(b,j,j+1)

where the test determines that the elements at positions j and j + 1 are not in the right order such

that it is necessary to swap the two elements by three assignments; the right diagram displays

an application where the test determines that the elements are already in the right order such

that no swap is necessary. The tag “Level 1” in the titles of the windows indicates that the

visualization refers to the application of an operation that was invoked on “Level 0”. If the

“Level 1” operation would involve another operation application, it would contain another call

node; by double-clicking on that node, we would move to “Level 2” and so on. A double click

on any empty part of the window moves the display back to the previous level.

By closing the window (via a click on the top right button of the window frame) the visualization

is terminated and the execution machine continues with the execution of the next invocation of

the operation being checked. By clicking on the button (Stop Execution) in the main window,

20

this process can be prematurely terminated (such that it is not necessary to step through the

visualizations of all possible calls of the operation).

The visualization of the execution trace of a procedure also displays the application of all

operations (typically functions and predicates) applied when checking the formal annotations

(pre- and postconditions, invariants, termination measures, assertions) of the procedure. If this

is not desired, those annotations should be temporarily commented out.

3 More Examples

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

3.1 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.3 for the full

speciﬁcation):

val N:Nat;

val M:Nat;

We make use of the following type deﬁnitions

type nat = Nat[M];

type array = Array[N,nat];

type index = Nat[N-1];

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

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

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

proc sort(a:array): array

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

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];

21

j := j-1;

}

b[j+1] := x;

}

return b;

}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proc main(): Unit

{

choose a: array;

print a, sort(a);

}

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

in “Deterministic” mode gives output

Run of deterministic function main():

[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]

22

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.

3.2 DPLL Algorithm

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

Loveland) algorithm for deciding the satisﬁability of propositional logic formulas with at most

n variables in conjunctive normal form. We start with the following declaration (the full speciﬁ-

cation is given in Appendix C.4):

val n: N;

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

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

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

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

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

type Literal = Z[-n,n];

type Clause = Set[Literal];

type Formula = Set[Clause];

type Valuation = Set[Literal];

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

Based on the predicate

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

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

23

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

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

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

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

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

respectively:

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

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

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

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

validity:

pred satisfiable(f:Formula) ⇔

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

pred valid(f:Formula) ⇔

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

We deﬁne the negation of a formula

fun not(f: Formula):Formula =

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

theorem notFormula(f:Formula)

requires formula(f);

⇔ formula(not(f));

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

satisﬁable:

theorem notValid(f:Formula)

requires formula(f);

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

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

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

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

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

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