Systematic refinement of abstract state machines with higher-order logic
Senén Andrés González Corenjo
José María Turull-Torres
T. Son Hoang
|Titel||Systematic refinement of abstract state machines with higher-order logic|
|Buchtitel||Abstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2018|
|Serie||Lecture Notes of Computer Science|
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.