Axiomatic Definitions of Programming Languages: A Theoretical Assessment
A precise definition is given of how partial correctness or termination assertions serve to define the semantics of classees of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of defining program scheme semantics, and effective axiom systems f...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/148990 |
| _version_ | 1826198153605414912 |
|---|---|
| author | Meyer, Albert R. Halpern, Joseph Y. |
| author_facet | Meyer, Albert R. Halpern, Joseph Y. |
| author_sort | Meyer, Albert R. |
| collection | MIT |
| description | A precise definition is given of how partial correctness or termination assertions serve to define the semantics of classees of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of defining program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic definitions are possible despite the limited expressive power of predicate calculus. |
| first_indexed | 2024-09-23T10:59:51Z |
| id | mit-1721.1/148990 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T10:59:51Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1489902023-03-30T03:57:16Z Axiomatic Definitions of Programming Languages: A Theoretical Assessment Meyer, Albert R. Halpern, Joseph Y. A precise definition is given of how partial correctness or termination assertions serve to define the semantics of classees of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of defining program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic definitions are possible despite the limited expressive power of predicate calculus. 2023-03-29T14:17:13Z 2023-03-29T14:17:13Z 1980-04 https://hdl.handle.net/1721.1/148990 6681993 MIT-LCS-TM-163 application/pdf |
| spellingShingle | Meyer, Albert R. Halpern, Joseph Y. Axiomatic Definitions of Programming Languages: A Theoretical Assessment |
| title | Axiomatic Definitions of Programming Languages: A Theoretical Assessment |
| title_full | Axiomatic Definitions of Programming Languages: A Theoretical Assessment |
| title_fullStr | Axiomatic Definitions of Programming Languages: A Theoretical Assessment |
| title_full_unstemmed | Axiomatic Definitions of Programming Languages: A Theoretical Assessment |
| title_short | Axiomatic Definitions of Programming Languages: A Theoretical Assessment |
| title_sort | axiomatic definitions of programming languages a theoretical assessment |
| url | https://hdl.handle.net/1721.1/148990 |
| work_keys_str_mv | AT meyeralbertr axiomaticdefinitionsofprogramminglanguagesatheoreticalassessment AT halpernjosephy axiomaticdefinitionsofprogramminglanguagesatheoreticalassessment |