Typechecking Z

Abstract. This paper presents some of our requirements for a Z typechecker: that the typechecker accept all well-typeable formulations, however contrived; that it gather information about uses of declarations as needed to support interactive browsing and formal reasoning; that it t the description given by draft standard Z; and that it be able to check some particular extensions to Z that are intended to allow explicit denitions of schema calculus operators. The paper presents a specication of such a Z typechecker, which we have implemented.

• Type: Conference
• Year: 2000
• Where: ZUM
• Authors: Ian Toyn, Samuel H. Valentine, Susan Stepney, Steve King
• Keywords: Draft Standard Z, Formal Methods, Schema Calculus Operators, Typechecker, ZUM 2000