Group:
machine model
Group:
meaning and truth
Group:
program proving
Topic:
decomposition of a system into levels
Topic:
evaluation in an environment
Topic:
formal methods and languages
Topic:
program execution
Topic:
program source as truth
Topic:
reduction languages
Topic:
requirement specification by assertion
Topic:
semantic truth; s iff p
Topic:
state machine
Topic:
virtual machine
| |
Summary
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 
| 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
| 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
| 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
| Quote: meta operators provide almost any semantic ability without changing the simple syntax of Red languages [»backJ_1972]
|
Subtopic: big-step semantics
| Quote: use big-step operational semantics to monitor reachable locations under the security policy [»leroX1_1998]
|
Subtopic: structural semantics
| 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
| 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
| 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
| Quote: fundamental semantic entities should reflect the computer's elementary operators
|
Subtopic: state machine system
| 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
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)
|
