article · 1994

Types and Sets in Gödel and Z - Unix File System Case Study

Margaret M. West

Cited by 0Abstract and details only

Abstract

An animation of a formal specification language is seen as a significant advantage in validating specifications. This paper the describes differences between the type systems of the programming language, Godel and the Z notation and the implications this has for devising a set of rules for animation of Z via Godel. A set of rules are outlined and future work is discussed whereby the correctness of the Godel implementation could be established. 1 Introduction The use of a formal specification produces significant advantages and an animated system model (or interpretation) provides an aid for developing and understanding such a specification. The animation may then be used for experiments and the results of the experiments can be used to assess and refine the design of the system. The draft IEC standard on industrial safety-related systems [1] states that the aim of prototyping/animation is: To check the feasibility of implementing the system against the given constraints. To c...

Cite this paper

APA 7

West, M. M. (1994). Types and Sets in Gödel and Z - Unix File System Case Study.

MLA 9

West, Margaret M. “Types and Sets in Gödel and Z - Unix File System Case Study.” 1994.

Chicago

West, Margaret M. 1994. “Types and Sets in Gödel and Z - Unix File System Case Study.”

Harvard

West, M.M. (1994) ‘Types and Sets in Gödel and Z - Unix File System Case Study’.

BibTeX

@article{west1994types,
  title = {{Types and Sets in Gödel and Z - Unix File System Case Study}},
  author = {West, Margaret M.},
  year = {1994}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.