. . . . . . . . . ( end of section Denotational Semantics) <<Contents | Index>>
. . . . . . . . . ( end of section Axiomatic Semantics) <<Contents | Index>>
They are not explicitly covered in our text.
. . . . . . . . . ( end of section Operational Semantics) <<Contents | Index>>
It should read (I guess)
s=0;
for(i=0; i<9; i++)
{
s = s+1;
}
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:
The above means "set x equal to 2* x and then add 1 to it", so if
then
means
By the way, doing functions this way turns out to simplify complex denotational formula.
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!
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 |
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
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.
variable := expression;Examples are:
i := i+1
f:=f*i
discriminant:= b^2 - 4*a*cThe '=' 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 := Emeans 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.
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 S2Is it the same as:
if ( c1 )
{ if (c2)
{
S1
}
}
else S2Or 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.
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.
a. e<<E+T>>s = e<<E>>s + e<<T>>sand we also have
c. e<<T>>s = a<<T>>sSo 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>>
Try Exercise 7!
. . . . . . . . . ( end of section Exercises) <<Contents | Index>>
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..
. . . . . . . . . ( end of section CSCI620 Session 5) <<Contents | Index>>