0541447 Tim Sheard Portland State University
Mitigating Human Error in Programs Through Combined Language/Reasoning Systems.
The theory and practice of combined programming/reasoning tools is investigated. The strategy is to enable programmers to define and reason about their programs, cast in terms of properties they defined themselves, all from within the programming language itself. The system developed will reason directly about programs (not models) using enhanced type systems to capture the properties of direct interest to the programmer. The project will develop a sound theory of combined programming/reasoning systems, and apply that theory by extending and refining the existing Omega language. The system will have four important characteristics that separate it from competing approaches. (1) Each property defined by the programmer has semantic meaning within the programming language independent of its role as a logical entity. (2) The systems separates values from types to maintain a familiar programming style. (3) Management of the constraints is performed inside the language using the well understood mechanism of constrained types. And, (4) The system partitions constraint management into static and dynamic parts, allowing the user to choose when constraints can be discharged at compile-time or at run-time. The broader impacts of combined programming/reasoning tools is to enable programmers to construct higher quality software. The reasoning capabilities allow an efficient division of labor: Experts design software by specifying its properties, and competent programmers fill in the details. The reasoning facilities check that the constructed software actually contains the desired properties.
