Proving entailment between conceptual state specifications

DOI10.1016/0304-3975(86)90007-1MaRDI QIDQ1095649zbMATH OpenOpenAlexFDO

Authors Eugene W. Stark

Publication date 1988

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(86)90007-1

zbMATH Keywords

concatenationconceptual state specificationsentailment between specificationsFIFO bufferssimulation between machinesspecification languagetemporal logic

Mathematics Subject Classification ID

Theory of operating systems (68N25) Data structures (68P05)

Review text

See the preliminary version in Lect. Notes Comput. Sci. 213, 197-209 (1986; Zbl 0587.68020).

Cites work

• Abstract data types and software validation
• scientific article; zbMATH DE number 3800906 (Why is no real title available?)
• Proof of correctness of data representations
• Proving Liveness Properties of Concurrent Programs
• Specifying Concurrent Program Modules
• Verifying temporal properties without temporal logic

Cited in

(4)

• Proving properties of states in the situation calculus
• Two implementation relations and the correctness of communicating replicated processes
• Application of the composition principle to unity-like specifications
• The existence of refinement mappings

This page was built for publication: Proving entailment between conceptual state specifications

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