@techreport{RISC5421,author = {Wolfgang Schreiner},
title = {{The RISC Algorithm Language - Tutorial and Reference Manual}},
language = {english},
abstract = {This report documents the RISC Algorithm Language (RISCAL). RISCAL is a language
and associated software system for describing (potentially nondeterministic) mathematical
algorithms over discrete structures, formally specifying their behavior by logical formulas
(program annotations in the form of preconditions, postconditions, and loop invariants),
and formulating the mathematical theories (by defining functions and predicates and stating
theorems) on which these specifications depend. The language is based on a type system
that ensures that all variable domains are finite; nevertheless the domain sizes may depend
on unspecified numerical constants. By instantiating these constants with values, all algo-
rithms, functions, and predicates become executable, and all formulas become decidable.
Indeed the RISCAL software implements a (parallel) model checker that allows to verify
the correctness of algorithms and the associated theories with respect to their specifications
for all possible input values of the parameter domains.},
year = {2017},
month = {January},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {70}
}