DocumentCode :
3014634
Title :
Applying a generalization of a theorem of Mills to generalized looping structures
Author :
Tchier, Fairouz ; Desharnais, Jules
Author_Institution :
Dept. of Math., King Saud Univ., Riyadh, Saudi Arabia
fYear :
1999
fDate :
1999
Firstpage :
31
Lastpage :
38
Abstract :
We present a generalization of a theorem of Mills, known as the while statement verification rule, that can be used to verify that a deterministic while loop computes a given function f. First, we study an abstract form of (nondeterministic) looping in the setting of relation algebras. We state a theorem showing how to verify that a given relation is the relation computed by the abstract loop. Then, we specialize this theorem to three forms of generalized looping structures that have been proposed in the literature, namely Dijsktra´s do od, Anson´s do upon and Parnas´ it ti. We take a demonic viewpoint; that is, we assume the worse possible execution of the nondeterministic programs under consideration
Keywords :
program verification; software engineering; Mills theorem; abstract loop; deterministic while loop; generalized looping structures; nondeterministic programs; relation algebras; while statement verification rule; Algebra; Concrete; Mathematics; Milling machines; Transformers;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Science and Engineering for Software Development: A Recognition of Harlan D. Mills' Legacy, 1999. Proceedings
Conference_Location :
Los Angeles, CA
Print_ISBN :
0-7695-0010-2
Type :
conf
DOI :
10.1109/SESD.1999.781109
Filename :
781109
Link To Document :
بازگشت