A Logic for Abstract State Machines
Дата
Авторы
Stärk,Robert
Nanchen,Stanislas
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
We introduce a logic for non distributed, deterministic Abstract State Machines with parallel function updates. Unlike other logics for ASMs which are based on dynamic logic, our logic is based on an atomic predicate for function updates and on a definedness predicate for the termination of the evaluation of transition rules. We do not assume that the transition rules of ASMs are in normal form, for example, that they concern distinct cases. Instead we allow structuring concepts of ASM rules including sequential composition and possibly recursive submachine calls. We show that several axioms that have been proposed for reasoning about ASMs are derivable in our system. We provide also an extension of the logic with explicit step information which allows to eliminate modal operators in certain cases. The main technical result is that the logic is complete for hierarchical (non-recursive) ASMs. We show that, for hierarchical ASMs, the logic is a definitional extension of first-order predicate logic.
Ключевые слова
Abstract State Machines , dynamic logic , modal logic , logical foundations of specification languages