{"id":{"repo_id":"sheffield-hallam","oai_identifier":"oai:shura.shu.ac.uk:19278"},"canonical_url":"https://search.dev.ndltd.org/etd/sheffield-hallam/oai:shura.shu.ac.uk:19278","repository":{"repo_id":"sheffield-hallam","name":"Sheffield Hallam University","base_url":"https://shura.shu.ac.uk/cgi/oai2"},"display":{"title":"Writing and animating Z specifications.","abstract":"The work presented in this thesis is concerned with the issues involved in writing and demonstrating formal specifications of information systems written in Z. The use of Z in software development, to enhance productivity and improve software quality, is not without its problems. Whilst the notation itself is highly developed, ways of systematically using Z to create specifications are, by contrast, poorly documented. Also, given that most commissioners of software are not skilled in reading Z, ways of demonstrating the important features of a formal Z specification to a customer are needed if the effective validation of the specification against user requirements is to take place. In this thesis we present a systematic approach, known as OPERATOR, for developing Z specifications and evaluate it against the issues identified for writing formal specifications. We also look at various ways of demonstrating Z specifications. We describe how Z specifications may be animated using Crystal, but go on to present a prototype CASE tool, known as Zappa, that may be used to create and demonstrate faithful animations of Z specifications. The thesis starts with a thorough review of software engineering and of the development and rise of formal methods. The development of the OPERATOR approach is then given along with a review of animation, a description of the Crystal technique, and the development of the CASE tool Zappa. An evaluation of the research against the stated aims is presented and areas where future research is needed are pointed out.","abstract_html":"The work presented in this thesis is concerned with the issues involved in writing and demonstrating formal specifications of information systems written in Z. The use of Z in software development, to enhance productivity and improve software quality, is not without its problems. Whilst the notation itself is highly developed, ways of systematically using Z to create specifications are, by contrast, poorly documented. Also, given that most commissioners of software are not skilled in reading Z, ways of demonstrating the important features of a formal Z specification to a customer are needed if the effective validation of the specification against user requirements is to take place. In this thesis we present a systematic approach, known as OPERATOR, for developing Z specifications and evaluate it against the issues identified for writing formal specifications. We also look at various ways of demonstrating Z specifications. We describe how Z specifications may be animated using Crystal, but go on to present a prototype CASE tool, known as Zappa, that may be used to create and demonstrate faithful animations of Z specifications. The thesis starts with a thorough review of software engineering and of the development and rise of formal methods. The development of the OPERATOR approach is then given along with a review of animation, a description of the Crystal technique, and the development of the CASE tool Zappa. An evaluation of the research against the stated aims is presented and areas where future research is needed are pointed out.","abstract_has_math":false,"creators":["Andrews, Simon John."],"institution":"Sheffield Hallam University (United Kingdom).","degree_name":"phd","degree_level":"doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":1996,"date_issued":"1996","date_published":"1996","updated_at":"2026-07-24T06:31:12Z","subjects":[],"languages":["en"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Andrews, Simon John."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["1996"]},{"key":"dc:date.issued","label":"Date","values":["1996"]},{"key":"dc:publisher.commercial","label":"Dc Publisher Commercial","values":["Sheffield Hallam University,"]},{"key":"dc:publisher.department","label":"Dc Publisher Department","values":["Department Not Provided."]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["Sheffield Hallam University (United Kingdom)."]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://shura.shu.ac.uk/19278/"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["phd"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://shura.shu.ac.uk/19278/1/10694158.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["The work presented in this thesis is concerned with the issues involved in writing and demonstrating formal specifications of information systems written in Z. The use of Z in software development, to enhance productivity and improve software quality, is not without its problems. Whilst the notation itself is highly developed, ways of systematically using Z to create specifications are, by contrast, poorly documented. Also, given that most commissioners of software are not skilled in reading Z, ways of demonstrating the important features of a formal Z specification to a customer are needed if the effective validation of the specification against user requirements is to take place. In this thesis we present a systematic approach, known as OPERATOR, for developing Z specifications and evaluate it against the issues identified for writing formal specifications. We also look at various ways of demonstrating Z specifications. We describe how Z specifications may be animated using Crystal, but go on to present a prototype CASE tool, known as Zappa, that may be used to create and demonstrate faithful animations of Z specifications. The thesis starts with a thorough review of software engineering and of the development and rise of formal methods. The development of the OPERATOR approach is then given along with a review of animation, a description of the Crystal technique, and the development of the CASE tool Zappa. An evaluation of the research against the stated aims is presented and areas where future research is needed are pointed out."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Writing and animating Z specifications."]}]}],"canonical_facts":{"dc:creator":["Andrews, Simon John."],"dc:date":["1996"],"dc:date.issued":["1996"],"dc:description.abstract":["The work presented in this thesis is concerned with the issues involved in writing and demonstrating formal specifications of information systems written in Z. The use of Z in software development, to enhance productivity and improve software quality, is not without its problems. Whilst the notation itself is highly developed, ways of systematically using Z to create specifications are, by contrast, poorly documented. Also, given that most commissioners of software are not skilled in reading Z, ways of demonstrating the important features of a formal Z specification to a customer are needed if the effective validation of the specification against user requirements is to take place. In this thesis we present a systematic approach, known as OPERATOR, for developing Z specifications and evaluate it against the issues identified for writing formal specifications. We also look at various ways of demonstrating Z specifications. We describe how Z specifications may be animated using Crystal, but go on to present a prototype CASE tool, known as Zappa, that may be used to create and demonstrate faithful animations of Z specifications. The thesis starts with a thorough review of software engineering and of the development and rise of formal methods. The development of the OPERATOR approach is then given along with a review of animation, a description of the Crystal technique, and the development of the CASE tool Zappa. An evaluation of the research against the stated aims is presented and areas where future research is needed are pointed out."],"dc:format":["application/pdf"],"dc:identifier.uri":["https://shura.shu.ac.uk/19278/1/10694158.pdf"],"dc:language":["en"],"dc:publisher.commercial":["Sheffield Hallam University,"],"dc:publisher.department":["Department Not Provided."],"dc:publisher.institution":["Sheffield Hallam University (United Kingdom)."],"dc:relation.isreferencedby":["https://shura.shu.ac.uk/19278/"],"dc:title":["Writing and animating Z specifications."],"dc:type":["Thesis"],"dc:type.qualificationlevel":["doctoral"],"dc:type.qualificationname":["phd"]},"updated_at":"2026-07-24T06:31:12Z"}