A language for building verified software components

Abstract

Safe and secure reuse is only achievable by deploying formally verified software components. This paper presents essential design objectives for languages for building such components and highlights key features in RESOLVE - a prototype for such languages. It explains why the language must include specifications as an integral constituent and must have clean and rich semantics, which preclude unconstrained aliasing and other unwanted side-effects. In order that arbitrarily complex components can be given concise and verification amenable specifications, an adequate language must also include an open-ended mechanism for incorporating additional mathematical theories. Given these essential characteristics, safe and secure reuse cannot be attained within popular languages, such as C++ or Java, either by constraining them or by extending them. Better languages are necessary. © 2013 Springer-Verlag Berlin Heidelberg.