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

    A Tactic Language for Reasoning About Z Specifications

    3rd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th September 1998


    I. Toyn


    The syntax and semantics of a particular tactic language are defined. The language uses lazy evaluation to manage backtracking in the search space.

    It also uses pattern matching to associate names with formulae that will subsequently be passed as arguments to an inference rule.

    The result of the inference rule is accompanied by a revision of the association, so that corresponding formulae in the result may be passed as arguments to the next inference rule.

    The combination of this revision with lazy evaluation raises some problems for efficient implementation.


    PDF filePDF Version of this Paper (254kb)