Title :
Refining logic programs using types
Author :
Colvin, Robert ; Hayes, Ian ; Strooper, Paul
Author_Institution :
Software Cerification Res. Center, Queensland Univ., Qld., Australia
fDate :
6/22/1905 12:00:00 AM
Abstract :
The logic programming refinement calculus is a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we show how types can be handled in the logic programming refinement calculus. Types of variables are necessary for a complete specification of a procedure, and typing information can guide the refinement of a procedure specification to code. As an application of this framework, we show how dynamic type-checks can be formally eliminated from a sample program
Keywords :
formal specification; logic programming; refinement calculus; code correctness; executable code; logic programs refinement; refinement calculus; specifications; types; typing information; Calculus; Computer science; Electronic mail; Logic programming;
Conference_Titel :
Computer Science Conference, 2000. ACSC 2000. 23rd Australasian
Conference_Location :
Canberra, ACT
Print_ISBN :
0-7695-0518-X
DOI :
10.1109/ACSC.2000.824379
