From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview
The advantages of denotational over operational semantics are argued. A denotational semantics is provided for an ALGOL-like language with finite-model procedures, blocks with local storage, and sharing (aliasing). Procedure declarations are completely explained in the ususal framework of complete p...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149056 |
| _version_ | 1826214989855195136 |
|---|---|
| author | Trakhtenbrot, B.A. Halpern, Joseph Y. Meyer, Albert R. |
| author_facet | Trakhtenbrot, B.A. Halpern, Joseph Y. Meyer, Albert R. |
| author_sort | Trakhtenbrot, B.A. |
| collection | MIT |
| description | The advantages of denotational over operational semantics are argued. A denotational semantics is provided for an ALGOL-like language with finite-model procedures, blocks with local storage, and sharing (aliasing). Procedure declarations are completely explained in the ususal framework of complete partial orders, but cpo's are inadequate for the semantics of blocks, and a new class of store models is developed. Partial correctness theory over store models is developed for commands which may contain calls to global procedures, but do not contain function procedures returning storable values. |
| first_indexed | 2024-09-23T16:14:30Z |
| id | mit-1721.1/149056 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T16:14:30Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1490562023-03-30T03:06:36Z From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview Trakhtenbrot, B.A. Halpern, Joseph Y. Meyer, Albert R. The advantages of denotational over operational semantics are argued. A denotational semantics is provided for an ALGOL-like language with finite-model procedures, blocks with local storage, and sharing (aliasing). Procedure declarations are completely explained in the ususal framework of complete partial orders, but cpo's are inadequate for the semantics of blocks, and a new class of store models is developed. Partial correctness theory over store models is developed for commands which may contain calls to global procedures, but do not contain function procedures returning storable values. 2023-03-29T14:23:37Z 2023-03-29T14:23:37Z 1983-10 https://hdl.handle.net/1721.1/149056 34602342 MIT-LCS-TM-246 application/pdf |
| spellingShingle | Trakhtenbrot, B.A. Halpern, Joseph Y. Meyer, Albert R. From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview |
| title | From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview |
| title_full | From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview |
| title_fullStr | From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview |
| title_full_unstemmed | From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview |
| title_short | From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: An Overview |
| title_sort | from denotational to operational and axiomatic semantics for algol like languages an overview |
| url | https://hdl.handle.net/1721.1/149056 |
| work_keys_str_mv | AT trakhtenbrotba fromdenotationaltooperationalandaxiomaticsemanticsforalgollikelanguagesanoverview AT halpernjosephy fromdenotationaltooperationalandaxiomaticsemanticsforalgollikelanguagesanoverview AT meyeralbertr fromdenotationaltooperationalandaxiomaticsemanticsforalgollikelanguagesanoverview |