Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Specification and Refinement in General Correctness

    3rd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th September 1998


    S. Dunne, A. Galloway & B. Stoddart


    We augment B's existing total-correctness semantics of weakest precondition (wp) with a partial-correctness semantics of weakest liberal precondition (wlp).

    By so doing we achieve a general-correctness semantics for B operations which not only accords more fully with our natural computational intuition, but also extends the essential expressive capability of B's Generalised Substitution Language (GSL) to embrace a whole new class of operations called semi-decidable, whose behaviour cannot be characterised in terms of total correctness alone.

    The ability to specify semi-decidable operations is important because a desired conventional operation may lend itself to implementation as a concurrent federation of semi-decidable operations co-operating under a mutual "termination pact".

    Indeed, computational constraints may render this the only viable implementation strategy. We call a generalised substitution invested with our general-correctness semantics an abstract command.

    Our Abstract Command Language (ACL) is thus syntactically indistinguishable from the GSL, save for the introduction of one new composition operator, concert, expressing a "termination pact" between two concurrent abstract commands.


    PDF filePDF Version of this Paper (223kb)