Select this to skip to main content [CSUSB] >> [CNS] >> [Comp Sci Dept] >> [R J Botting] >> [CSci620] >> 05 [Source]
[Index] [Schedule] [Syllabi] [Text] [Labs] [Projects] [Resources] [Search] [Grading]
Tue Apr 13 17:50:55 PDT 2004

Contents


    CSCI620 Session 5

      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 nameFull name
        Syntax
        ProgPrograms (made of statements etc)
        ConConditions (in statements)
        StmtStatements (in programs)
        ExprExpressions (in expressions)
        TerTerms in expressions (as in algebra)
        FacFactors in terms (as in algebra)
        Semantics
        NNumbers
        BBooleans
        FiFile! In Pascal all input output is via a file -- in this case of numbers
        CFConfiguration -- state plus input plus output
        StState 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

  1. BNF::="Backus-Naur Form", for syntax and grammar, developed by Backus and Naur.
  2. EBNF::="Extended " BNF.
  3. HTML::= "HyperText Markup Language", used on the WWW.
  4. HTML_page::syntax= "<HTML>" head body.
  5. Java::="An " OO " Language from Sun".
  6. LISP::= "LISt Processing Language".
  7. LRM::="Language Reference Manual".
  8. OO::="Object-Oriented".
  9. Prolog::="Programming in Logic".
  10. TBA::="To Be Announced".
  11. UML::="Unified Modeling Language".
  12. URL::=Universal_Resource_Locator,
  13. Universal_Resource_Locator::syntax= protocol ":" location, where
    Net
    1. protocol::= "http" | "ftp" | "mailto" | ... ,
    2. location::= O( "//" host) O(pathname).

    (End of Net)
  14. WWW::= See http://www.csci.csusb.edu/dick/cs620/, index to web site for this class.
  15. XBNF::="eXtreme" BNF, developed by the teacher from EBNF, designed to ASCII input of syntax, semantics, and other formal specifications.


Formulae and Definitions in Alphabetical Order