Systematic refinement of abstract state machines with higher-order logic

Autoren Flavio Ferrarotti
Senén Andrés González Corenjo
Klaus-Dieter Schewe
José María Turull-Torres
Editoren M. Butler
A. Raschke
T. Son Hoang
K. Reichl
Titel Systematic refinement of abstract state machines with higher-order logic
Buchtitel Abstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2018
Typ in Konferenzband
Verlag Springer
Serie Lecture Notes of Computer Science
Band 10817
ISBN 978-3-319-91270-7
DOI 10.1007/978-3-319-91271-4_14
Monat June
Jahr 2018
Seiten 204-2018
SCCH ID# 18016
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.