Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6806
Title: Language Features that Support Program Verification (illustrated in PL/C)
Authors: Constable, Robert L.
Keywords: computer science
technical report
Issue Date: Apr-1976
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR76-276
Abstract: The author of a program can convince its readers (including himself) that it computes as he intended by writing into the program text a precise description of what it should do. This description can include a clear proof that the program behaves as advertised. In the future, programming languages may offer far more mechanical assistance in expressing, checking, and processing these descriptions than they do now. However, some existing languages, such as PL/C, provide features which help in these tasks considerably. Here we examine such features applied to simple programs of the type traditionally taught in beginning programming classes. We discuss various proposals for expanding programming languages to provide more assistance of this type. Keywords and phrases: program correctness, automatic program verification, Hoare axioms, Scott induction, recursive programs, least number operator, bounded quantifiers, inductive assertion method, programming language design, very high level programmng languages, PL/I, PL/C, macro facilities.
URI: http://hdl.handle.net/1813/6806
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
76-276.pdf1.44 MBAdobe PDFView/Open
76-276.ps571.56 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us