SEMANTICS (Q1,'05)
[ semantics | relevance | roles | structure | schedule | exercises | project | exam | re-exam | materials | classes | webboard ]

SEMANTICS EXAM (FALL 2005)

  • Period: [ Wednesday 19/10 @ 12:00 -- Friday 21/10 @ 20:00 ]

  • The exam features 4 (four) exercises of almost equal weight: (20-30%):
    • 1. Static and dynamic semantics for a stack-based language [30%];
    • 2. Proof of a semantic property (via structural induction) [25%];
    • 3. Equivalences of CCS processes (weak and strong bisimilarity) [20%];
    • 4. Implementation of a dynamic semantics (complete a "fill-in the blanks-implementation") [25%].

  • Individual exam:
    • This is an exam; the exercises must be solved individually (i.e. not in groups)!

  • Grading:
    Be sure to motivate, explain, and argue for the reasoning behind your solutions! Be concise and to the point (not necessarily "the more explanation the better"); include only issues relevant to the problem at hand (irrelevant issues may subtract points).

    All this is what wins you the points (i.e. there are no/very few points for unmotivated solutions "out-of-the-blue", correct or not).

    The actual grading is done relative to the course objectives; i.e., that you demonstrate the ability:

    • to describe formally the meaning of a wide range of programming constructs;
    • to explain fundamental concepts, techniques, and results regarding formal semantics of programming languages;
    • to implement semantic descriptions in familiar programming languages;
    • to analyze the meaning of a wide range of programming constructs;
    • to compare semantic descriptions;
    • to reason about semantic descriptions;
    • to prove consequences of semantic descriptions; and
    • to apply all above skills to concrete programs (to understand and prove properties of programs).

    ...whereever relevant.

  • Handing-in:
    Submit your solution (in Danish or English) to the exam assignments by copying it into your delivery directory (which is a directory owned by you for the duration of the exam and which is located here): 
        /users/courses/dSem/exam/<<username>>/        (e.g. /users/courses/dSem/exam/brabrand/ )
    no later than (Friday 21/10 @ 20:00) at which point the delivery directories will be closed (and handed over to me). You may not change the permissions of the directory.

    Handing in must be according to the following convention:

    You place the files exactly as shown below (do not in-line your ML implementation(s) in the report; we need to be able to run them and do not deliver any other temporary or binary files): 

        /users/courses/dSem/exam/<<username>>/exam.pdf (xor "exam.doc")
                                         /BEE.sml             // cf. exercise 4
                                         /trace.bee.txt       // cf. exercise 4
                                         /BEER.sml            // cf. exercise 4
                                         /trace.beer.txt      // cf. exercise 4

  • If you write the SOS rules by hand (which is fine as long as you write them very(!) clearly), then you need to scan them into PDF (the University printers can do this).

  • Alternatively, you may hand in a hardcopy (by putting your report in the big red hand-in-box in the hall of the Babbage building) no later than (Friday 21/10 @ 20:00); however, you still have to deliver the trace and ML program files as specified above (also before the deadline).

  • Your report must have your name and your student-id on the front page. If you use Word, do not use non-standard fonts (e.g., special non-standard mathematical fonts).

    Violations of any of the above rules will subtract points.

  • Damage control:
    If you run out of time or cannot solve an exercise, identify and restrict your solution to a suitable subset (make this clear in your hand-in). This will, of course, reduce your grade (but at least you will get some points instead of none for no solution). In particular; for the programming exercise: submit your (ML) program even if it may not be fully operational (you may still get points for the things that would work with a bit of "tweaking").

EXERCISE 0 (IMPORTANT INFORMATION)

  • Read the information at the top of this document thorougly, as it is likely to indirectly improve your grade (in making sure you do not lose points by missing important information)!

EXERCISE 1 (STATIC AND DYNAMIC SEMANTICS FOR A STACK-BASED LANGUAGE)

Consider the following stack-based language, STK (without variables):

  • -) The syntax of a STK program is given by the syntactic category, P (which is in turn defined in terms of STK commands as given by the syntactic category, C): 
        P   :   exec C           // execute command C (with an initially empty stack)
    
    C   :   noop             // no-operation (does nothing)
        |   push n           // push constant integer n onto the stack
        |   add              // pop two top elements from the stack, add them, and push the result
        |   mul              // pop two top elements from the stack, multiply them, and push the result
        |   C ; C'           // sequential execution of C and C'
        |   ifz C else C'    // pop top element from the stack, execute C if it was zero (C', if not)

  • a1) Give the signatures (for all relations you plan to use in assignment "a2" below):

  • a2) Give a reasonable static semantics for the STK language, making sure that:
    • -) for all P programs (exec C), the execution of C always results in a stack of height 1 (for "the result");
    • -) for all P programs, add and mul are never executed with a stack height of less than 2 (two); and
    • -) branching along either control-flow path of the ifz-construction (i.e. C and C') always produces the same resulting stack height.

      [ Hint: You may, for instance, use (possibly among other things) a command well-formedness relation, |-wfc, relating a command, C, an assumed initial stack height, n, and a resulting stack height, m (e.g., "|-wfc C:n:m") ]

  • b1) Give the configurations, terminal configurations, and signature of the transition relation (for all transition systems you plan to use in assignment "b2" below). Also, in case you are using any intermediate syntax, introduce it explicitly by giving the new grammar for P and C with the intermediate syntax added (if you are using any).

  • b2) Give a reasonable small-step structural operational dynamic semantics for the STK language as informally described (in gray color) above.

    [ Hint: For configurations, you may wish to use (possibly among other things) <C,w> (where C is a command, and w (omega) is an integer sequence (stack) belonging to Z* ]

    [ Hint': Also, you may wish to use the syntactic conventions that "ε" (epsilon) describes the empty integer sequence (empty stack), and "n::w" describes the concatenation of integer n and integer sequence w (omega) ]

[ 30% ]

EXERCISE 2 (PROOF OF SEMANTIC PROPERTY VIA STRUCTURAL INDUCTION)

Proof of termination for a non-Turing-Complete, non-deterministic, small expression language, MultChoice:
  • Syntax: Let the syntax of MultChoice expressions Exp (ranged over by E) be given by: 
        E   :   z   |   E * E   |   E ? E : E
  • Semantics: Let the small-step structural operational semantics (SOS) of MultChoice expressions be given by:

    MultChoice configurations

    MultChoice small-step structural operational semantics (SOS)

  • Definition: Let the "size" of a MultChoice expressions be given by the following inductive definition:

    MultChoice "size" signature and definition

  • a) Give the sizes of the following programs:

    • 1) 1*2 (i.e. give: |1*2|)
    • 2) (1?2:3) (i.e. give: |(1?2:3)|)
    • 3) (0*(1?2:3)?4*5:6*7) (i.e. give: |(0*(1?2:3)?4*5:6*7)|)

  • b) Give the proof structure for assignment "c" below:

  • c) Prove the following property (by structural induction):

    MultChoice property

  • Note (for your information): That this property is satisfied means that any MultChoice program will terminate since the "size" measure can be used as a so-called "termination function" on derivation sequences. The requirement for a termination function is that it is a strictly decreasing injection into the non-negative natural numbers (for any sequence). The "size" of a given expression initially starts out at some non-negative integer value v, and then strictly decreases with each evaluation step until it reaches zero (precisely when the expression is completely evaluated). Since there are finitely many natural numbers between v and zero, the number of evaluation steps must be (upper-)bounded by v. This argument may be illustrated as follows:

    Illustration of argument for guaranteed termination

    It is (of course) impossible to construct a (strictly decreasing) termination function for the L language due to the "while-do" construction (no termination function would strictly decrease). This note was not an exercise, but purely for your information (why the above property is a proof of termination).

[ 25% ]

EXERCISE 3 (CCS AND BISIMILARITY)

Bisimilarity of CCS processes (or labelled transition systems):
  • -) Consider the following processes definitions: 

        SYS   =def   b.0 + (a.0 | 'a.0) [b/a] \ { b }

    A   =def   x.tau.0
    A'  =def   tau.x.0

    B   =def   tau.0 + (x.0 | 'x.0) \ { x }
    B'  =def   tau.0

    C   =def   x.(tau.0 + y.P)
    C'  =def   x.0 + x.y.P

  • a) Give all derivation sequences for the SYS process (above).

  • b) Decide whether the following claims are true or false and support your above claims, using either (strong) bisimulation games or the definition of strong bisimilarity.
    • 1) A ~ A' (i.e., A and A' are strongly bisimilar)?
    • 2) B ~ B' (i.e., B and B' are strongly bisimilar)?
    • 3) C ~ C' (i.e., C and C' are strongly bisimilar), for all processes P?

  • c) Decide whether the following claims are true or false and support your above claims, using either (weak) bisimulation games or the definition of weak bisimilarity.
    • 1) A ~~ A' (i.e., A and A' are weakly bisimilar)?
    • 2) B ~~ B' (i.e., B and B' are weakly bisimilar)?
    • 3) C ~~ C' (i.e., C and C' are weakly bisimilar), for all processes P?

  • d) Suppose the two CCS processes, IMPL and SPEC are observationally equivalent (aka. weakly bisimilar); i.e., IMPL ~~ SPEC. Argue that we have the following relationship: 
        a . IMPL [f] | P \ L   ~~   a . SPEC [f] | P \ L

    for all actions, a, renaming functions, f, processes, P, and labelling sets, L.

[ 20% ]

EXERCISE 4 (PROGRAMMING OF DYNAMIC SEMANTICS)

Consider the "Bit Evaluation Engine" (aka. The BEE Language) with two syntactic categories Bsq, bit sequences (ranged over by "B"), and Exp, expressions (ranged over by "E"):
  • Syntax: Let the syntax of the BEE language be given by: 
        B   :   0   |   1   |   B 0   |   B 1                              // Bsq: bit sequences

    E   :   [ B ]   |   E + E   |   out E   |   ( E , E )   |   z      // Exp: expressions
    Where the z (for a mathematical number in Z) in Exp is intermediate syntax for fully evaluated bit sequences (used in the semantics below).

  • Semantics (Bsq): Let the structural operational semantics (SOS) for Bsq (bit sequences) be given by:

    Bsq signature

    Bsq structural operational semantics (SOS)

  • Semantics (Exp): Let the small-step structural operational semantics (SOS) for Exp (expressions) be given by:

    Exp configurations

    Exp small-step structural operational semantics (SOS)

  • Fill-in-the-blanks-implementation: Here is a complete implementation of the BEE language containing everything except the implementation of the semantic rules [ONE], [B-ZERO], and [B-ONE] (for Bsq) and [BITS], [PLUS3], [OUT1], [OUT2], [SEQ1], and [SEQ2] (for Exp); these rules just raise exceptions in their present form.

  • Note: The "fill-in-the-blanks-implementation" can be downloaded here: 

        [ http://www.daimi.au.dk/semantics/BEE.sml ]
    ...and the implementation contains: [ overview ].

  • a) Complete the implementation by implementing rules [ONE], [B-ZERO], and [B-ONE] (for Bsq) and [BITS], [PLUS3], [OUT1], [OUT2], [SEQ1], and [SEQ2] (for Exp); and explain the rules informally (i.e., what are the consequences of the the rules as they are defined for Bee programs). Submit along with the report, your completed implementation; i.e., the file: "BEE.sml".

  • b) Run and submit the stepwise output trace for the following BEE program, BP (and briefly explain what happens); submit along with the report, the output trace as a file: "trace.bee.txt": 

        BP   =   out (out ([00] + [01]), (out [10]) + (out [11]))

  • c) Write the SOS rules for a semantic variant of the language (known as "Bit Evaluation Engine Reversed"; aka. The BEER Language) in which the addition, "E+E'", and sequence, "(E,E')", operators evaluate their expressions right-to-left (i.e., both are to evaluate E' before E). You only have to give the SOS rules for the changed parts (the actually modified SOS rules).

  • d) Now make a copy of your BEE implementation and change it according to your SOS rules (in assignment "c") above to obtain an implementation for the BEER language variant. Submit along with the report, the file: "BEER.sml".

  • e) Re-run and submit the stepwise output trace on the above BP program, but now interpreted as a BEER program (and briefly explain what happens in comparison with assignment "b" above). Submit along with the report, the output trace as a file: "trace.beer.txt".

[ 25% ]

EXERCISE 0 (CONT'D)

  • Re-read the information at the top of this document thorougly, as it is likely to indirectly improve your grade (in making sure you do not lose points by missing important information)!

CURRICULUM ("PENSUM")

Lectures: [ slides: 1 | 2 | 3 | 4 | 5 | 6 | 7 ]
Reading: [ SOS (Chap.1-3, p.1-78) ] + [ CCS (Chap.1-5, p.1-63) ] + [ Note on Induction ]
Exercises: [ exercises: 1 | 2 | 3 | 4 | 5 | 6 ] + [ project ]

October 2005

Mo Tu We Th Fr Sa Su
17 18 19 20 21 22 23

Claus Brabrand (October 19, 2005)