| Operational Semantics |
Article Index for Operational |
Website Links For Operational |
Information AboutOperational Semantics |
| CATEGORIES ABOUT OPERATIONAL SEMANTICS | |
| formal specification languages | |
| logic in computer science | |
| semantics | |
|
In Computer Science , operational semantics is a way to give meaning to Computer Program s in a mathematically rigorous way (See Formal Semantics Of Programming Languages ). The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps. These sequences then ''are'' the meaning of the program. In the context of Functional Program s, the final step in a terminating sequence returns the value of the program. (In general there can be many computation sequences and many return values for a single program, because the program could be Nondeterministic .) A common way to rigorously define the operational semantics, pioneered by Gordon Plotkin in his 1981 paper "A Structural Approach to Operational Sematics", is to provide a State Transition System for the language of interest. Such a definition allows a formal analysis of a language, permitting the study of Relations between programs. Important relations include Simulation Preorder s and Bisimulation . These are especially useful in the context of Concurrency . Another approach to the semantics of concurrency is using event structures as in the Actor Model . Defining operational semantics through a state transition system is usually done by giving an Inductive Definition of the set of possible transitions. This usually takes the form of a set of Inference Rule s which define the valid transitions in the system. The first operational semantics was that of the Lambda Calculus . Abstract machines in the tradition of the SECD Machine are closely related. REFERENCES
|
|
|