Axioms for behavioural congruence of single-pass instruction sequences

DOI10.7561/SACS.2017.2.111MaRDI QIDQ4621212zbMATH OpenFDO

Authors J. A. Bergstra, C. A. Middelburg

Publication date 8 February 2019

Published in Scientific Annals of Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1702.03511

zbMATH Keywords

program algebrastructural congruenceaxiom systembehavioural congruenceinstruction sequence congruence

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and complete axiom systems for the first two congruences were already given in early papers on program algebra. The current paper is the first one that is concerned with an axiom system for the third congruence. The presented axiom system is especially notable for its axioms that have to do with forward jump instructions.

Recommendations

• Program algebra for sequential code
• On the expressiveness of single-pass instruction sequences
• A short introduction to program algebra with instructions for Boolean registers
• Program algebra for component code
• On the behaviours produced by instruction sequences under execution

Cited in

(2)

• On the expressiveness of single-pass instruction sequences
• On the complexity of the correctness problem for non-zeroness test instruction sequences

This page was built for publication: Axioms for behavioural congruence of single-pass instruction sequences

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4621212)