Istituto di Scienza e Tecnologie dell'Informazione     
Aiello L., Aiello M., Weyhrauch R. Program correctness checked by machine: the reliability of a reservation system. Internal note IEI-B75-25, 1975.
An axiomatization in LCF of a substantial subset of PASCAL (including I/O) is presented. The correctness of a program for the " McCarthy Airline" reservation system is then stated and proved in this axiomatization. An interesting aspect of such a program is that it deals with a potentially infinite sequence of inputs. The statement of the LCF theorem asserting its partial correctness and the machine.checked proof of a such a theorem (carried out using the Stanford LCF proof-checker) are presented and discussed.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional