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 |

1) Download Document PDF |

Open access Restricted Private