Systematic refinement of abstract state machines with higher-order logic

F. Ferrarotti, J. Turull-Torres. Systematic refinement of abstract state machines with higher-order logic. volume 10817, pages 204-2018, DOI 10.1007/978-3-319-91271-4_14, 6, 2018.

Autoren
  • Flavio Ferrarotti
  • José María Turull-Torres
BuchAbstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2018
TypIn Konferenzband
VerlagSpringer
SerieLecture Notes of Computer Science
Band10817
DOI10.1007/978-3-319-91271-4_14
ISBN978-3-319-91270-7
Monat6
Jahr2018
Seiten204-2018
Abstract

Graph algorithms that involve complex conditions on subgraphs can be specified much easier, if the specification allows expressions in higher-order logic to be used. In this paper an extension of Abstract State Machines by such expressions is introduced and its usefulness is demonstrated by examples of computations on graphs, such as graph factoring and checking self-similarity. In a naive way these high-level specifications can be refined using submachines for the evaluation of the higher-order expressions. We show that refinements can be obtained in an automatic way for well-defined fragments of higher-order logic that collapse to second-order, by means of which the naive refinement is only necessary for second-order logic expressions.