PUMA
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.
 
 
Abstract
(English)
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.
Subject


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