Steadfast logic programs
1999 (English)In: The journal of logic programming, ISSN 0743-1066, E-ISSN 1873-5789, Vol. 38, no 3, 259-294 p.Article in journal (Refereed) Published
We present the notion of steadfastness that at once embodies modularity, reusability, and formal correctness. A steadfast program is an open program with parameters, which is parametrically correct in the sense that it will always be correct with respect to its (open) specification whenever its parameters are computed correctly. Thus, a steadfastprogram is correct, modular and reusable. Therefore, steadfastness provides a basis for hierarchical construction of correct reusable modules. We first introduce the idea of steadfastness in an informal manner. Then we give a model-theoretic characterisation of steadfastness, followed by an operational semantics based on the (open) completion of an open program. Finally, we apply our general results to program correctness with respect to parametric specifications.
Place, publisher, year, edition, pages
1999. Vol. 38, no 3, 259-294 p.
Correctness, modularity, reusability, open programs, parametric programs, parametric specifications, specifications, institutions, semantics
Computer and Information Science
IdentifiersURN: urn:nbn:se:uu:diva-40656DOI: 10.1016/S0743-1066(98)10023-7ISI: 000078199000001OAI: oai:DiVA.org:uu-40656DiVA: diva2:68557