Topic: semantics by an abstract machine

topics > computer science > programming > Group: program representation

machine model
meaning and truth
program proving

decomposition of a system into levels
evaluation in an environment
formal methods and languages
program execution
program source as truth
reduction languages
requirement specification by assertion
semantic truth; s iff p
state machine
virtual machine


The semantics of high-level languages are defined by an abstract machine. For instance, underlying Algol is an 'Algol' machine. PL/1 was specified in Vienna Definition Language, and Pascal semantics were defined by axiomatic specification. In each case some form of abstract environment, which associates identifiers with values, is modified through language statements. Scott and Strachey provide one of the most solid semantic basis; but all such representations are complex, especially for replacement with its necessarily non-reversible semantics. (cbb 5/80)

Formal semantics have not been as important as anticipated. Perhaps because of their dynamic nature. Languages tend to ignore the underlying state transitions. In a way, an abstract machine is no better than a real machine for many purposes. (cbb 12/92)

Subtopic: operational semantics up

Quote: relying on intuition about the meaning of names is dangerous or almost impossible; need to specify the operational semantics of a type [»guttJV6_1977]
Quote: operational semantics treats a program as an instruction sequence on the states of a machine [»degaP6_2001]
Quote: a formal definition of semantics requires a process of interpretation and a representation of information [»floyRW2_1964]
Quote: programming language semantics was very descriptive; only told how to hand-simulate a program
Quote: to interpret the semantics of computer behavior must see it as operating on symbols [»pylyZW_1986]
Quote: most languages are secondary; their semantics employ a independent state language; meaning is execution of state machine [»backJ_1972]
Quote: operational semantics are good formal methods; intuitive, help implementers, simple, easy prototyping, easy integration [»degaP6_2001]
Quote: most texts explain control structures by tracing execution of some implementation, even though this is frowned upon in general [»hehnEC_1977]
Quote: define a programming language using a phrase structure syntax and interpretation rules; one-to-one correspondence to a parse; applied to a generalization of ALGOL [»wirtN1_1966]

Subtopic: machine state vs. environment up

Quote: environment is the set of variables modified by the programming language; defines the meaning of a sentence [»wirtN1_1966]
Quote: one machine state and multiple environments; environment only altered by the variable binding operator [»straC1_1974]

Subtopic: denotational semantics up

Quote: denotational semantics of goto statements as continuations; rudimentary language allows goto during expression evaluation [»straC1_1974]
Quote: separate mathematical semantics from the operational semantics; define imperative and dynamic features as change-of-state functions on machine states [»straC1_1974]

Subtopic: meta operators up

Quote: meta operators provide almost any semantic ability without changing the simple syntax of Red languages [»backJ_1972]

Subtopic: big-step semantics up

Quote: use big-step operational semantics to monitor reachable locations under the security policy [»leroX1_1998]

Subtopic: structural semantics up

Quote: structural operational semantics via proved transition systems; a transition is an encoding of its deduction tree [»degaP6_2001]
QuoteRef: neuhEJ2_1971 ;; shows formal language used to describe PL/1 syntax and semantics--operate on program in tree form. goes into detail

Subtopic: compositional semantics up

Quote: operational semantics requires execution sequence; must have compositionality or definitions become ad hoc [»degaP6_2001]
Quote: sequential execution is function composition; a neat, simple model with deterministic results [»leeEA5_2006]
Quote: structural operational semantics recovers compositionality through the syntactic structure of the language [»degaP6_2001]
Quote: use combinators to find the value of a financial contract; compositional, abstract valuation semantics [»joneSP9_2000]

Subtopic: semantics by abstract machine up

Quote: gives a formal definition of Pascal using a very large set of axioms and inference rules [»hoarCA11_1972]
Quote: abstract C-- defines a formal semantics that hides registers, calling convention, instruction set, spills, register shuffles, value passing registers, and the stack of activation records [»ramsN6_2000]
Quote: formal definition of Euler with translator and interpreter for an abstract machine; derived from Algol [»wirtN1_1966]
Quote: use continuations to handle side effects, abnormal exits, and gotos [»tennRD8_1976, OK]
QuoteRef: hoarCA2_1974 ;;139 interpretive model-- abstract machine with control function (eg Vienna definition
QuoteRef: kostCH_1974 ;;378 defines simple abstract machine and writes programs for it [well worked out examples

Subtopic: abstract machine vs. actual machine up

Quote: fundamental semantic entities should reflect the computer's elementary operators

Subtopic: state machine system up

Quote: while the environment may behave mathematically, the machine state behaves operationally; state transformations are essentially irreversible [»straC3_1973]
Quote: use analytic syntactic functions and state vectors to define the semantics of a programming language; e.g., val(t) and mkconst(val(t)) [»mccaJ8_1962]
Quote: could describe Algol as set of legal programs, initial states, and mappings between programs and state changes [»backJ_1973, OK]
Quote: during evaluation of an applicative expression, a state is a stack, environment, control, and a dump; (S, E, C, D) [»landPJ1_1964]
Quote: a language has a state language when its domain is a set of computations that define the reduction operator [»backJ_1973]
Quote: state-machine paradigm represents state by values of storage variables; must handle simultaneous assignment [»floyRW8_1979]
Quote: interpretation of programming languages depends on the dynamic state of the system; more complex mathematically [»scotD8_1971]
QuoteRef: hoarCA2_1974 ;;142 computation model--memory state sequence through recursion on sub-parts of statement [like this one]
QuoteRef: hoarCA2_1974 ;;146 deductive theory--describe memory state properties before and after each statement [like this one]
QuoteRef: kuznOP6_1972 ;;state transition (asynchronous diagrams split into blocks with input and output constraints

Related Topics up

Group: machine model   (13 topics, 206 quotes)
Group: meaning and truth   (18 topics, 634 quotes)
Group: program proving   (10 topics, 311 quotes)

Topic: decomposition of a system into levels (49 items)
Topic: evaluation in an environment (35 items)
Topic: formal methods and languages (53 items)
Topic: program execution (8 items)
Topic: program source as truth (17 items)
Topic: reduction languages (17 items)
Topic: requirement specification by assertion (28 items)
Topic: semantic truth; s iff p (34 items)
Topic: state machine (67 items)
Topic: virtual machine
(13 items)

Updated barberCB 6/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.