Abstract
We discuss how the specification of the PLAN programming language supports the design objectives of the language. The specification aims to provide a mathematically precise operational semantics that can serve as a standard for implementing interpreters and portable programs. The semantics should also support proofs of key properties of PLAN that would hold of all conformant implementations. This paper discusses two such properties. (1) Type checking is required, but interpreters are given significant flexibility about when types are checked; the specification must support a clear description of the possible behaviors of a network of conformant implementations. (2) It is essential to have guarantees about how PLAN programs use global resources, but the specification must be flexible about extensions in the network service layer. We illustrate on of kind of issue that will arise in using to specification to prove properties of the network based on the choice of services.
Original language | English (US) |
---|---|
Pages (from-to) | 87-104 |
Number of pages | 18 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 26 |
DOIs | |
State | Published - 1999 |
Externally published | Yes |
Event | HOOTS '99, Higher Order Operational Techniques in Semantics - Paris, France Duration: Sep 30 1999 → Oct 1 1999 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science