This paper explores the connection between the Smyth power domain PS(D) of a domain D and the domain D itself. The Smyth power domain is the most prevalent of the three power domain constructions commonly used to mode...
详细信息
This paper discusses some fundamental issues related to the construction of semantically based axiomatic proof systems for reasoning about program behavior. We survey foundational work in this area, especially early w...
详细信息
ISBN:
(纸本)9783540190202
This paper discusses some fundamental issues related to the construction of semantically based axiomatic proof systems for reasoning about program behavior. We survey foundational work in this area, especially early work of Hoare and Cook on while-programs, and we try to pinpoint the principal ideas contained in this work and to suggest criteria for an appropriate generalization (faithful to these ideas) to a wider variety of programminglanguages. We argue that the adoption of a mathematically clean semantic model should lead to a natural choice of assertion language(s) for expressing properties of program terms, and to syntax-directed proof systems with clear and simple rules for program constructs. Hoare's ideas suggest that in principle syntax-directed reasoning is possible for all syntactic categories (declarations, commands, even expressions) and all semantic attributes (partial correctness of commands, aliasing properties of declarations, L- or R-values of expressions, proper use of variables, and so on). Semantic insights may also influence assertion language design by suggesting the need for certain logical connectives at the assertion level. This point is obscured by the fact that Hoare's logic for while-programs needed no assertion connectives (although of course the usual logical connectives are permitted inside pre- and post-conditions), but an application of our method to a class of parallel programminglanguages brings out the idea well: semantic analysis suggests the use of conjunctions at the assertion level. We argue that this method can lead to proof systems which avoid certain inelegant features of some earlier systems: specifically, we avoid the need for "extralogical" and "non-compositional" notions such as interference checks and auxiliary variables. We also discuss the author's applications of these techniques to other programminglanguages, and point to some future research directions continuing this work. Although we do not have a completel
Miranda has two interesting features in its typing system: implicit polymorphism (also known as ML-style polymorphism) and algebraic types. Algebraic types create new types from old and can operate on arbitrary types....
详细信息
This paper demonstrates a notion for formal semantics specification of concurrent programminglanguages and applies it to the concurrent part of the programminglanguage Ada. The abstract syntax of an Ada program is g...
详细信息
This volume is the proceedings of the 3rd workshop on the mathematical foundations of programming language semantics held at Tulane University, New Orleans, Louisiana, April 8-10, 1987. The 1st workshop was at Kansas ...
详细信息
ISBN:
(数字)9783540389200
ISBN:
(纸本)9783540190202
This volume is the proceedings of the 3rd workshop on the mathematical foundations of programming language semantics held at Tulane University, New Orleans, Louisiana, April 8-10, 1987. The 1st workshop was at Kansas State University, Manhattan, Kansas in April, 1985 (see LNCS 239), and the 2nd workshop with a limited number of participants was at Kansas State in April, 1986. It was the intention of the organizers that the 3rdworkshop survey as many areas of the mathematicalfoundations of programminglanguagesemantics as reasonably possible. The workshop attracted 49 submitted papers, from which 28 papers were chosen for presentation. The papers ranged in subject from category theory and Lambda-calculus to the structure theory of domains and power domains, to implementation issues surrounding semantics.
暂无评论