Paper Info
Title
Nondeterministic Flowchart Programs With Recursive Procedures - Semantics And Correctness .1.
Abstract
In this paper, we study some aspects of the semantics of nondeterministic flowchart programs with recursive procedures. In the first part of this work we provide the operational semantics of programs using the concept of an execution tree. We propose a new definition of the semantics of a non-deterministic recursive program as a mapping from the input domain to the set of execution trees determined by the program. Using this new concept, we prove that every nondeterministic flowchart program with recursive procedures can be unfolded into a semantically equivalent infinite pure flowchart (without procedures). This result is applied in the second part of this work to prove the soundness of an inductive assertion method which is also complete with a finite number of assertions (contrary to De Bakker and Meertens's method [11]).
Year
DOI
Venue
1981
10.1016/0304-3975(81)90039-6
THEORETICAL COMPUTER SCIENCE
DocType
Volume
Issue
Journal
13
2
ISSN
Citations 
PageRank 
0304-3975
3
0.70
References 
Authors
0
1
Name
Order
Citations
PageRank
Jean H. Gallier1749111.86