 Why Don’t Programming Language Designers Use Formal Methods?
started 8/24/2002; 2:49:11 AM - last post 8/27/2002; 3:44:48 AM
|
|
jon fernquest - Why Don’t Programming Language Designers Use Formal Methods? 
8/24/2002; 2:49:11 AM (reads: 2015, responses: 2)
|
|
| Why Don’t Programming Language Designers Use Formal Methods? |
|
An argument for Action Semantics.
Discusses the life cycles of some languages
(Pascal , ADA-83, ML) and how they failed to use
formal specifications until long after they'd
actually been specified.
Action Semantics emphasizes pragmatics and can specify
the semantics of imperative, object-oriented, functional, and
concurrent programming languages.
...these specifications are unusually writable, modifiable, reusable, and readable.
These qualities are consequences of the design of action notation. Familiar
programming language concepts like binding, storing, sequencing, iteration, etc.,
are directly expressed in action notation....an action-semantic specification
reads rather like an operational specification expressed in English.
There is also an
Action Semantics home page
that has three well-written tutorials:
Also note that Action Semantics influenced Espinosa's Scheme monad-based
Semantic Lego
("Why Don’t Programming Language Designers Use Formal Methods?",
David A. Watt, 1996)
Posted to implementation by jon fernquest on 8/24/02; 3:23:25 AM
|
|
|
|
jon fernquest - Re: Why Don’t Programming Language Designers Use Formal Methods?
8/27/2002; 3:44:48 AM (reads: 884, responses: 0)
|
|
|
The semantic lego <-> action semantics connection:
Peter Mosses describes action semantics, a reformulation of his theory of ab-
stract semantic algebras. Mosses attempts to achieve modularity in semantics by defining an
intermediate level, called actions, into which one can translate language constructs. Actions
are low-level enough to be flexible, but high-level enough to hide the details of interactions
between facets of a language.
Since Mosses has not yet been able to combine facets, he gives a single algebra of actions,
with environments, stores, etcetera. This algebra corresponds to a single stratified monad
generated by the toolkit. Mosses's theory is more modular than pure denotational semantics
because constructs are isolated from each other, but, from our point of view, it is not modular
at all. One can only define modularly the constructs that the algebra was designed to define.
That is, one can define stores modularly because the fixed algebra of actions includes modular
stores.
Recalling that Moggi cites Mosses's comments on the non-modularity of denotational
semantics, we can more gently view the toolkit as a final step in Mosses's program. Stratified
monads could be the modular facets Mosses was looking for.
From:
("Building Interpreters by Transforming Stratified Monads",
David Espinosa, 1994)
Can't find anything extending Espinosa's work. Is Espinosa's work a dead end or are people still interested in his ideas?
|
|
|
|