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 naïve 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 naïve refinement is only necessary for second-order logic expressions.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{FerrarottiGST18,
author = {Flavio Ferrarotti and
Sen{\'{e}}n Gonz{\'{a}}lez and
Klaus{-}Dieter Schewe and
Jos{\'{e}} Maria Turull Torres},
editor = {Michael J. Butler and
Alexander Raschke and
Thai Son Hoang and
Klaus Reichl},
title = {Systematic Refinement of Abstract State Machines with Higher-Order
Logic},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10817},
pages = {204--218},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-91271-4\_14},
doi = {10.1007/978-3-319-91271-4\_14},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/FerrarottiGST18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}