Access Restriction

Author Winikoff, Michael ♦ Dart, Philip ♦ Kazmierczak, Ed.
Source CiteSeerX
Content type Text
Publisher Springer-Verlag
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Description . There is growing interest in animating formal specifications for the purpose of better understanding the requirements and for validating the specification. Formal specifications in a non-executable language offer challenges for animation systems, for example, dealing effectively with infinite data sets, sensibly animating functions which are not computable and determining a sensible set of inputs and outputs for arbitrary relations. In this paper we examine these issues in the context of animating Z specifications in the logic programming language Mercury. In particular we outline how information for making a non-executable Z specification executable can be derived using static analysis techniques from logic programming. We present analysis algorithms for deriving control (mode) and representation (subtype) information and show how these analyses are used in a tool for deriving Mercury programs from Z specifications. Finally we compare our approach with existing systems for animating...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1998-01-01
Publisher Institution In Proceedings of the 21st Australasian Computer Science Conference