Paper Info
Title
Hoare's logic for nondeterministic regular programs: a nonstandard approach
Abstract
This paper studies Hoare's logic for nondeterministic regular programs (with unbounded nondeterminism) from the point of view of nonstandard dynamic logic. We define a so-called continuous semantics which allows certain “infinitely long computations” and compare it with usual semantics, proving among other things the equivalence of both over “reasonable data types”. We also establish a completeness theorem for Hoare's calculus relative to continuous semantics, thereby generalizing a previous result of Csirmaz. The proof makes use of a normal form for regular programs which is perhaps interesting in its own right.
Year
DOI
Venue
1989
10.1016/0304-3975(89)90165-5
Theor. Comput. Sci.
Keywords
DocType
Volume
nonstandard approach,nondeterministic regular program
Journal
68
Issue
ISSN
Citations 
3
Theoretical Computer Science
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
M. T. Hortala-Gonzalez100.34
Mario Rodríguez-Artalejo271659.70