Wolfgang Schreiner,
"The RISC Algorithm Language - Tutorial and Reference Manual"
, Serie RISC Report Series, Johannes Kepler University Linz, Austria, RISC, JKU, Hagenberg, Linz, 1-2017
Original Titel:
The RISC Algorithm Language - Tutorial and Reference Manual
Sprache des Titels:
Englisch
Original Kurzfassung:
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 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 speci?cations for all possible input values of the parameter domains.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
RISC, JKU
Verlagsanschrift:
Hagenberg, Linz
Serie:
RISC Report Series, Johannes Kepler University Linz, Austria
Forschungs-