MENDELS ZONE has put formal methods into practical use as described 
above, and it becomes possible to verify the correctness of specifications and 
transform them into programs. As a result, reliable programs can be gener-
ated. 

OUTLINE OF SYSTEM 

The development of programs using MENDELS ZONE has two phases, 
namely, the "Algebraic Specification Phase" in which objects are generated 
and the "Petri Net Phase" in which Objects are composed. 

Figure 1 is a snapshot taken during the "Algebraic Specification Phase".




FIGURE 1 


Users denote algebraic specifications for behavior Method of objects . In 
order to describe specifications correctly, MENDELS ZONE provides several 
support functions: syntactical check, direct execution as a term rewriting 
system and verification with inductionless induction. When equations that the 
specifications should satisfy are given in , the system verifies automatically 
whether they are true or not. Progress of the verification procedure can be 
observed in . After verification, the specifications are transformed into 
MENDEL objects automatically. 

Figure 2 is a snapshot taken during the "Petri Net Phase". Objects gener-
ated by automated transformation are registered in a Parts-Library . Com-
position of objects is represented in terms of a high-level Petri net (MENDEL 
net), and is created using only mouse operations in the graphical MENDEL 
net editor . In general, there are some timing constraints among methods in 


					- 99 -