A Logic for the Russell Programming Language
| dc.contributor.author | Boehm, Hans-J. | en_US |
| dc.date.accessioned | 2007-04-23T16:50:29Z | |
| dc.date.available | 2007-04-23T16:50:29Z | |
| dc.date.issued | 1984-02 | en_US |
| dc.description.abstract | We consider a programming language with a number of characteristics detrimental to conventional axiomatic descriptions. These include arbitrary side effects in expressions, aliasing among variables, very general recursive function declarations, and the ability to pass functions as parameters and return them as results. We give an axiomatic definition of this language based on a novel formalism. We prove the axiomatization sound and relatively complete with respect to a (somewhat nonstandard) denotational semantics. In spite of the nonstandard formalism, most conventional techniques for developing and reasoning about programs can be carried over. (ABRIDGED) | en_US |
| dc.format.extent | 6269264 bytes | |
| dc.format.extent | 1796297 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-593 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6433 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | A Logic for the Russell Programming Language | en_US |
| dc.type | technical report | en_US |