A Concurrent Specification of POSIX File Systems Technical Report

In this section we formalise the assertion language, the assertion model, the specification language and the associated semantics of refinement. We establish an adequacy theorem (theorem 1) justifying our refinement relation with respect to an operational semantics. The semantics and proofs are inspired by the earlier work of Turon and Wand [?] and follow a similar structure. Major differences arise from our combination with TaDA [?], as the assertion model and the atomicity semantics are entirely different. We then define general refinement laws, refinement laws for atomicity and encode the concept of hybrid specification statements that combine atomic and non-atomic effects and define associated refinement laws, and show that they are sound. ∗gian.ntzik@amadeus.com †pmd09@doc.ic.ac.uk ‡jhs110@doc.ic.ac.uk §pg@doc.ic.ac.uk