Un sistema per la produzione e la verifica di programmi strutturati

The paper describes a system supporting production and verification of programs in a structured programming environment. The system is based on a logical formalism for describing the semantics of the employed programming language and of programs. An interpreter of the formalism is provided which on one hand allows the execution of partially specified programs, and on the other hand is able to prove properties of programs. Thus, at any level of the top-down development, programs can be executed and proved correct. An example of program development is given and discussed.