Название: Concrete Abstractions: Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker
Автор: Wolfgang Schreiner
Издательство: Springer
Год: 2023
Страниц: 278
Язык: английский
Формат: pdf (true)
Размер: 10.1 MB

This book demonstrates how to formally model various mathematical domains (including algorithms operating in these domains) in a way that makes them amenable to a fully automatic analysis by computer software.The presented domains are typically investigated in discrete mathematics, logic, algebra, and Computer Science; they are modeled in a formal language based on first-order logic which is sufficiently rich to express the core entities in whose correctness we are interested: mathematical theorems and algorithmic specifications. This formal language is the language of RISCAL, a “mathematical model checker” by which the validity of all formulas and the correctness of all algorithms can be automatically decided. The RISCAL software is freely available; all formal contents presented in the book are given in the form of specification files by which the reader may interact with the software while studying the corresponding book material.

The goal of this book is to demonstrate how we can formally model various mathematical domains (including algorithms operating in these domains) in a way that makes them amenable to a fully automatic analysis by computer software. These domains are typically investigated in subjects such as discrete mathematics, logic, algebra, and computer science; they are modeled in a formal language that encompasses the language of first-order logic (predicate logic) which is sufficiently rich to express the core entities in whose correctness we are interested: mathematical theorems and algorithmic specifications.

However, most model checkers do not analyze mathematical domains and algorithms, but hardware and software systems; for these, they verify properties that are either fixed (such as the freedom from runtime errors) or specified in logics with limited expressiveness (such as propositional logic or temporal propositional logic) or in logics with special scope (such as relational logic). A major exception is Leslie Lamport’s concurrent system modeling language TLA+ and the associated algorithm language PlusCal where specifications are expressed in temporal first-order logic. Generally, however, the languages of most model checkers make them not very attractive for dealing with mathematical domains.

On the contrary, RISCAL (RISC Algorithm Language) has been developed for this very purpose (with some inspiration taken from TLA+). RISCAL is a “mathematical model checker” with a language that allows to formalize a mathematical theory in a statically typed variant of classical first-order logic and set theory. The model of the theory is parameterized with respect to its size; by assigning concrete values to the model parameters we derive a finite instance in which the validity of all formulas and the correctness of all algorithms can be automatically decided. For this purpose, RISCAL translates formulas and algorithms into an executable representation of their denotational semantics that is evaluated in the model instance; alternatively, the system may also translate a first-order formula interpreted over this instance into a quantifier-free formula interpreted over a decidable theory; the validity of this formula can be then checked by employing some external SMT (satisfiability modulo theories) solvers.

We start with an exposition of the themes that are central to this book: mathematical theories and their theorems, computational problems in these theories, and algorithms that solve these problems. For this purpose, we shall in the Chapter 1 focus on the theory of (a certain kind of) numbers, the problem of computing the greatest common divisor (gcd) of two numbers, and the ancient Euclidean algorithm that computes the gcd. In our elaboration, we assume a moderate amount of familiarity with the RISCAL software and refer for this purpose the reader to Appendix A.

Contents:





ОТСУТСТВУЕТ ССЫЛКА/ НЕ РАБОЧАЯ ССЫЛКА ЕСТЬ РЕШЕНИЕ, ПИШИМ СЮДА!