Previous

[ 04.html ]

Preparation

Study chapter 3 on semantics pages 48 to 64 inclusive. Prepare some notes and at least one question you need to ask on it.

Denotational Semantics

Did you spot the errors on pages 56 to 59?

. . . . . . . . . ( end of section Denotational Semantics) <<Contents | Index>>

Axiomatic Semantics

We don't have time for this .... sadly. Any one feel like presenting a paper on Hoare's original paper?

. . . . . . . . . ( end of section Axiomatic Semantics) <<Contents | Index>>

Operational Semantics

Operational semantics can be informal (using a natural language), based on an abstract or virtual machine, or provide a set of derivation rules for reasoning about the states of a program.

They are not explicitly covered in our text.

. . . . . . . . . ( end of section Operational Semantics) <<Contents | Index>>

Questions

On page 63 is the Java in question 5 correct

No.

It should read (I guess)

 		s=0;

 		for(i=0; i<9; i++)

 		{

 			s = s+1;

 		}

What are injection and projection

These are casting operations in domains, see [ Injection and Projection on Sum Domains in 04 ]

Equation t rearranges the order of statement pairs -- why is o like this

The o composition operator was in use in mathematics before high level computer languages existed. The definition was
1. (f o g)(x) = f(g(x)).

   Thus the mathematical operator for composing functions works from right to left: g first, f second.

   This clashes with the way Algol, Pascal, etc composed statements:

2. x:=2*x; x:=x+1;

   The above means "set x equal to 2* x and then add 1 to it", so if

3. f = multiply x by 2
4. g = add 1 to x

   then

5. x:=2*x; x:=x+1;

   means

6. do f and then do g = g o f.

   By the way, doing functions this way turns out to simplify complex denotational formula.

   Does the degree symbol mean append on pages 52 etc.

   Not really. It is a form of the composition operator for functions. See previous question for a definition.

   Why have two strings in a configuration, shouldn't one do

   The configuration domain is a triple:

    		class Configuration { State state; string input; string output;};

   In theory you could pack both into one string. But we need to separate the input from the output so that we know where one starts and the other stops!

   Define the abbreviated names for domains

   Short name	Full name
   Syntax
   Prog	Programs (made of statements etc)
   Con	Conditions (in statements)
   Stmt	Statements (in programs)
   Expr	Expressions (in expressions)
   Ter	Terms in expressions (as in algebra)
   Fac	Factors in terms (as in algebra)
   Semantics
   N	Numbers
   B	Booleans
   Fi	File! In Pascal all input output is via a file -- in this case of numbers
   CF	Configuration -- state plus input plus output
   St	State of the memory: In each state we record the value of its variables

   Explain the axiom of consequence on page 60

    		if S implies P and P{Q}R then S{Q}R.

   Suppose some one has written some code and they tell you that it works for all values of x greater than 0. Then, you know that if x is 10 it will work. This is because
7. if x=10 then x>0.

    		if P{Q}R and R implies S then P{Q}S.

   Suppose that the code we are talking about has the property that when it finishes it gives you an integer y such that y>20. Then we know that y is also greater than 0!

   Note: Axioms should be obvious.... when looked at the right way, unfortunately in any interesting system there is an axiom that looks most doubtful and over complex.

   Explain := etc on page 48

   In the Algol family of languages (Algol, Pascal, Ada, ...) assignment is shown using the := operator, like this.

    		variable := expression;

   Examples are:

    		i := i+1

    		f:=f*i

    		discriminant:= b^2 - 4*a*c

   The '=' symbols is used to test equality in conditions.

    		expression = expression;

   This symbol

    		::=

   is used to define syntax. It is a meta-symbol. It is not part of the language we are defining.

   The := symbol is a vital part of the languages Algol, Pascal, Ada,...

    		S ::= V := E

   means that a statement S can be an assignment statement that starts with a variable V, is followed by the assignment operator (:=), and finishes with any expression E.

   Is it an ambiguity when you can write an algorithm in different ways in a language

   No.

   Ambiguity occurs when a statement has two or more possible meanings and you can not determine which is correct. In the early days of Algol 60 there was a classic ambiguity. Consider the following C/C++/Java code:

    		if(c1) if (c2) S1 else S2

   Is it the same as:

    		if ( c1 )

    		{	if (c2)

    			{

    				S1

    			}

    		}

    		else S2

   Or is it:

    		if ( c1 )

    		{	if (c2)

    			{

    				S1

    			}

    			else S2

    		}

   In the first Algol 60 report you could not tell. By the 1964 revision the syntax had been rewritten... to stop the ambiguity. Ever since then language syntax definitions are very careful not to let this happen.

   So ambiguity is when we have one string with many meanings.

   Having many strings that have the same use/meaning is normal.

   Equations f, h, and i on page 49 and page 51

   Here is each with the Greek written in English:

    		f. a<<F>> s = b<<F>> s.

   This means that if a term is actually a factor F then the 'b' rules should be used to evaluate F.

    		h. b<<cons>>s = element of N corresponding to cons.

   This means that if our factor is a constant like "123" or "42" then it means the integer corresponding the that string of digits. This rule is an abbreviation of many rules describing how to calculate the meaning of decimal numerals.

    		i. b<<V>>s = s[V]

   This rule says that if we have a factor that is actually a variable then we must look in the array of variable and look up the current value of that variable.

   Explain why a on page 49 doesn't user alpha

   We have an equation

    		a. e<<E+T>>s = e<<E>>s   + e<<T>>s

   and we also have

    		c. e<<T>>s   = a<<T>>s

   So we can derive a new rule that combines both an a and c into one rule:

    		ac. e<<E+T>>s = e<<E>>s   + a<<T>>s

   However the tradition in theory is to do things is very small obviously correct steps rather than bigger ones. It is likely (but this is my guess) that the book's form is more stable if we made changes to a language. I'm also sure that the a form is found in the original papers and books on the topic!

. . . . . . . . . ( end of section Questions) <<Contents | Index>>

Exercises

Evaluating denotations using equations.

Try Exercise 7!

. . . . . . . . . ( end of section Exercises) <<Contents | Index>>

Laboratory

You should go to [ while.html ] and study it. This is a definition of a WHILE-like language with a few extras. I have provided an abstract syntax and the semantics.

By the end of the lab session I expect each person to have found something different wrong with it..... a typographical error, a spelling mistake, bad grammar, a bad link, something that is unclear, etc..

Next

Study Chapter 4 pages 65..87 lexical and syntactic translators [ 06.html ]

. . . . . . . . . ( end of section CSCI620 Session 5) <<Contents | Index>>

Glossary