ISSN:
1433-299X
Keywords:
Verification
;
Functional logic
;
Intensional logic
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract In many areas of computation and reasoning, the value of an expression may depend on an implicit parameter, which may for example represent a program state, or time, or a possible world. In this paper we describe a formal first order logic which captures a general notion of expressions which depend on an implicit parameter. Both semantics and syntax are discussed. An important application of the logic, used as a running example, is to provide a basis for unifying the Hoare logic of procedural programs with the mathematically powerful techniques of classical logic and set theory. It is, however, beyond the scope of this paper to develop this application fully.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01211079
Permalink