Proving entailment between conceptual state specifications

DOI10.1016/0304-3975(86)90007-1zbMath0632.68026OpenAlexW1525901496MaRDI QIDQ1095649

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

temporal logicspecification languageconcatenationconceptual state specificationsentailment between specificationsFIFO bufferssimulation between machines

Mathematics Subject Classification ID

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

Related Items

Application of the composition principle to unity-like specifications ⋮ Two implementation relations and the correctness of communicating replicated processes ⋮ The existence of refinement mappings

Cites Work

• Unnamed Item
• Proof of correctness of data representations
• Specifying Concurrent Program Modules
• Verifying temporal properties without temporal logic
• Proving Liveness Properties of Concurrent Programs
• Abstract data types and software validation