Complementing semi-formal specifications with Z
		Yves Ledru (Yves.Ledru@imag.fr)


The insertion of formal techniques into the daily practice of software
engineering definitely improves the quality of specifications.  An
approach is proposed where semi-formal specifications are translated
into the formal specification language Z and enriched by formal
annotations.  The paper starts from a specification of an access
control system in terms of classical description techniques:
entity-relationship schemas, data-flow diagrams, and state machine
descriptions.  It shows how these descriptions can be combined with
formal definitions of types, constraints and functions.