DocumentCode :
2136566
Title :
Facilitating program verification with dependent types
Author :
Xi, Hongwei
Author_Institution :
Dept. of Comput. Sci., Boston Univ., MA, USA
fYear :
2003
fDate :
22-27 Sept. 2003
Firstpage :
72
Lastpage :
81
Abstract :
The use of types in capturing program invariants is overwhelming in practical programming. The type systems in languages such as ML and Java scale convincingly to realistic programs but they are of relatively limited expressive power. In this paper, we show that the use of restricted form of dependent types can enable us to capture many more program invariants such as memory safety while retaining practical type-checking. The programmer can encode program invariants with type annotations and then verify these invariants through static type-checking. Also, the type annotations can serve as informative program documentation, which are mechanically verified and can thus be fully trusted. We argue with realistic examples that this restricted form of dependent types can significantly facilitate program verification as well as program documentation.
Keywords :
formal specification; program verification; system documentation; type theory; Java language; ML language; dependent types; memory safety; program documentation; program invariants; program verification; type systems; type-checking; Computer languages; Computer science; Documentation; Functional programming; Java; Programming profession; Runtime; Safety; Scalability; Solids;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on
Conference_Location :
Brisbane, Queensland, Australia
Print_ISBN :
0-7695-1949-0
Type :
conf
DOI :
10.1109/SEFM.2003.1236209
Filename :
1236209
Link To Document :
بازگشت