Una tecnica di specifica basata sull'integrazione di Sadt e Z

Structured specification techniques are based on informal graphical notations which perform well in managing the complexity of the task of requirement specification; specifications written using such notations are easy to "talk about" but hard to reason about and to be automatically checked, due to a lack of formal semantics in the notations. Conversely, formal specifications could be in principle reasoned about, but are hard to understand and to "talk about", due to the weakness of the structuring mechanisms and to their not very appealing mathematical flavour. The integration of structured and formal specification techniques is emerging as a strategy for bringing together the advantages of both classes of techniques while reducing their drawbacks. This work aims at a possible integration of a well known structured specification technique, namely SADT, with a well known formal specification language, namely Z. The goal is achieved through a subset of SADT, called ASA, whose formal semantics is easily provided in Z. A normal form of ASA specifications is shown, and a translation of SADT into ASA is provided.