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

Contents


    CSCI620 Session 4

      Previous

      [ 03.html ]

      Preparation

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

      Denotational Semantics

        Basics

        Denotational semantics defines a set of maps that take syntactic forms and provides meanings for them. For example suppose that d is a semantic map providing meanings for binary strings:
        Net
        1. d<<"0">> = 0.
        2. d<<"1">> = 1.
        3. d<<x "0">> = 2 d<<x>> .
        4. d<<x "1">> = 2 d<<x>> +1 .

        (End of Net)
        This is how d defines the meaning of "101":
        Net
        1. d<<"101">>
        2. = 2 d<<"10">> + 1
        3. = 2(2*d<<"1">>) + 1
        4. = 2*(2*1)+1
        5. = 2*2+1
        6. = 4+1
        7. = 5.

        (End of Net)
        Commonly the meaning of something is defined in terms of the meaning of its parts. For example, the meaning of "a=2*b+1;" in C/C++/Java depends on the meaning of "a" and "2*b+1", Because it is an assignment it means evaluate 2*b+1 and put the resulting value in the location of a.

        Metalanguage

          Symbols for Undefined and Over-defined

          These special symbols are used to indicate things that have know meaning.
        1. top::= symbol for something that is over defined.
        2. bot::=symbol for an undefined meaning.

          Comment on chapter 3

          I'm not too happy with the definitions of domains, products and so on. I'm raiding some other books and will add my definitions to this page.

          Some books and papers use a simpler definition of domain than Scott and Strachey did. This omits the top (over-defined) element but keeps the bot element. I wrote some notes on this some years ago and put them on the web [ math_24_Domains.html ] in the mathematical part of my web site.

          Domain

          A domain is always more than a normal "set".

          A domain is created by
          Elementsdefining a set of elements in it,
          Top, bottomidentifying (or adding) the top and bot of the domain.
          Orderdefining an order that we interpret as "is less defined than".
          (An order must be transitive, etc...) such that top is more defined than any other element, and bot is less defined than all other elements.

          For example the domain N of numbers in the book is defined by
          ElementsAll the integers including negatives and zero.
          top...The bot and top symbols.
          OrderFor all numbers n, bot is less defined than n and top is more defined than n. All numbers are equally defined: neither more or less defined than each other.

          Given a normal set S (with no top or bot)

        3. S^o::= following domain,
          ElementsS
          Top...top, bot
          OrderFor all x in S, bot is less defined than x and x is less defined than top.

          Product Domains

          Figure 3.4 in the book is correct. The example of B><V on page 42 is incorrect.

          Given two domains A and B the product domain is defined by

        4. A><B::=following domain
          Elements{ (a,b). for each a:A and b:B } -- including (bot, x) for example.
          -bot := ( A.bot, B.bot ), top := (A.top, B.top).
          OrderFor a1,a2:A, b1,b2:B, (a1,b1) is less defined than (a2,b2) if and only if a1 is less defined than a2 and b1 is less defined than b2.
          Note that for sets S1 and S2, if D1=S1^o and D2=S2^o then D1><D2 is not the same as (S1 >< S2)^o.

          Where the book uses a downward pointing arrow.... most people would use a simple subscript.

          The test does not waste time distinguishing (A><B)><C from A><(B><C) because in set theory and domain theory they are isomorphic (same thing in disguise). It flattens them to (A><B><C).

          Simple Power Domains

          Taking products of a domain with itself gives us powers:
        5. A^0 = {bot, (), top).
        6. A^1 = A.
        7. A^2 = A><A.
        8. A^3 = A><A><A.
        9. and so on.

          Sum Domains

          These are also called disjoint unions. The idea is to define a domain that contains a copy of one domain and a separate copy of the other --- even if they have overlapping elements.

          Given a couple of domains A and B the sum domain is defined as

        10. A+B::=following domain
          Elements{ (a,1). for a:A } | { (b,2). for b:B }.
          " (A.bot,1), (A.top, 1), (B.bot,2), and (B.top,2) are all in this domain.
          -Add new top and bot elements.
          OrderFor a1, a2: A, (a1,1) is less defined than (a2,1) if a1 is less defined than a2.
          "For b1, b2: B, (b1,2) is less defined than (b2,2) if b1 is less defined than b2.
          "(a,1) and (b,2) are not less or more defined than each other.
          "For all (x,i), bot is less defined than (x,i) and (x,i) is less defined than top.

          Infinite Sum Domains

          Now we have powers and sums we can define
        11. A^*::= {()} + A + A^2 + A^3 +... and Scott and Strachey have shown that this is a meaningful "limit" ...

          Functions

          Used for modeling memory state, and many other things.

          A function (or power domain) of two domains A and B can be defined by

        12. A -> B::=following domain
          Elements{ f. for all a:A, one b:B ( f(a) = b ) }.
          -Add bot and top as functions than map every a:A in bot and top respectively.
          OrderFor f,g: A->B, f is less defined than g if for all a:A ( f(a) is less defined than g(a) ).

          Lists

          These are defined using the above function. I'd call them string operations!

          Operators on Domains

          We now have an algebra of domains with product, sum, and powers/functions.

          Injection and Projection on Sum Domains

          The book defines some useful notations/ideas for sum domains.

          The book defines projection (|)and injection (in) operators. These are just like up and down casting operations in an OO language like C++. Suppose we had a domain Number which was the sum of Int and Float domains:

        13. Number = Int + Float. Then 1.234 is an element of Float, but (1.234 in Number) is an element of Number. Howver suppose we had a number x that is a Number, then it may be an Int or it may be a Float. x|Int is meaningful if x is an Int and is the value of x as an Int. Similarly with x|Float.

          A condition that make sure that an element is in a particular part of the sum: For x:D1+D2+....+D[i]+..., x E D[i]::x is in D[i].

          Changing Functions

          Functions are going to be used to model storage. We need there to be able to change their values (change the value stored in a location). The book uses a common notation f[b/a] for this.
          xf(x)
          ab
          elsef(x)
          I tend to misread this and so write f[a+>b] ::= f[a:=b]. f[a:=b] ::= the f' where for all x(if x=a then f'(x)=b else f'(x) = f(x)).

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

        Simple Semantic Equations

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

      Questions

        Why do we need precise semantics

        As programmers, compiler writers, consultants, and teachers we need to be able to answer questions about statements in programming languages. Semantics handles questions about what something in a language means. Precise semantics mean we can find out precisely what is ment by a piece of a program.

        Notice we can not rely on the compiler or a vendor to define the meaning of a language. The result allows programs to suddenly start misbehaving as their meaning changes.

        Trying to us ENglish in a standard has lead to langauges that are paradoxical ... the meanings contradict each other, or undefined -- we can not figure out what a staement or expressions means. Formal (mathematical and/or logical) methods have tended to provide clear answers to questions and early indicators of error in a language specification.

        What is the a on line 5 of Page 44

        It is an example of a character. It is an element
      1. of the domain C. Since C is a subset of C* the a is also a member of C*.

        Similarly lines 3 and 4 show a member of I and of R (real).

        So each line is a member of (I+ C* + R).

        So, all three lines is a sequence in (I + C* + R)*

        Can you give examples of D1->D2 on page 44.

        A Function domain is used to model the behavior of storage.

        Suppose we have a domain of variable names Var and a domain of values Val, then storage is modelled as

      2. Var -> Val. Commonly the values can be different types: bool, int, float,... and
      3. Var -> (Bool + Int + Float).

        So if s:Var->(Bool+Int+FLoat) we might have

      4. s(test) = true.
      5. s(i) = 42.

        Another common example is modelling changes to State. Each change is a function mapping the past into the present:

      6. State -> State.

        Explain the notations of Page 46.

        The in and | operators are very like casts in C++ the change the type of an expression fro the special to the general or back again.

        Explain Maps from Syntax to Semantics

        A Semantic map is a function that takes a piece of syntax and gives us the meaning of the syntax in return. For example if we had a language with a skip statement that did nothing, and Id is the identity map, then we can define a map
      7. "skip" +> Id Or more formally
      8. m<<skip>> = Id.

        Explain the notation on page 39.

        The key notation is like this:
      9. name_of_semantic_map << piece_of_syntax >> which describes the result of applying the map to the syntax.

        Is there an error in Figure 3.5

        YES! The bot[B] symbol in the left hand side of the lattice should be \bot[L].

        Explain a Lattice.

        A lattice is a mathematical algebra based on two operators called the least upper bound (supremum) and greatest lower bound (infimum). I have got some documentation on lattices that can be found via: [ lookup.php?search=lattice ]

        Lattice are a useful way of looking at many things and have been recently used in sofware engineering. Here is a pretty example [ Programming_Languages in logic_42_Properties_of_Relation ] that describes languages and how they are related.

        On page 45 explain the notation

        The notation
      10. s:S means that S is a set or domain and s is an element in the set or domain.

        In the example given

      11. s: S= Operators -> ( (C><C) -> N ) we have a set of maps that take an operator like "+" and tell us how it works. The particular s can be applied to "+" and the result applied to two C's to give an N
      12. s[+](4,3).

        I think the book's formula s[+(3,4)] is wrong.

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

      Examples

      Using semantic equations to evaluate expressions. Page 41.

      Semantic Equations
      Net

      1. (a): e<<E+T>> = e<<E>> + e<<T>>.
      2. (b): e<<E-T>> = e<<E>> - e<<T>>.
      3. (c): e<<T>> = a<<T>>.
      4. (d): a<<T*F>>= a<<T>> * a<<F>>.
      5. (e): a<<T/F>>= a<<T>> / a<<F>>.
      6. (f): a<<F> = b<<F>>
      7. (g): b<<(E)>> = (e<<E>>).
      8. (h): b<<constant>> = some value in the integers.

      (End of Net)

      Determining the meaning of 3*2+1. Note, in my notation on web pages the steps in a proof are linked to the rules that were applied.
      Net

      1. e<<3*2+1>>
      2. (parsing) |-
      3. = e<<(3*2)+1>>
      4. (a) |-
      5. = e<<(3*2)>> + e<<1>>
      6. (c) |-
      7. = e<<(3*2)>> + a<<1>>
      8. (f) |-
      9. = e<<(3*2)>> + b<<1>>
      10. (h) |-
      11. = e<<(3*2)>> + 1
      12. (c) |-
      13. = a<<(3*2)>> +1
      14. (f) |-
      15. = b<<(3*2)>> +1
      16. (g) |-
      17. = (e<< 3*2 >> ) +1
      18. (c) |-
      19. = (a<<3*2>>) +1
      20. (d) |-
      21. = (a<<3>>*a<<2>>) +1
      22. (f, f) |-
      23. = (b<<3>>*b<<2>>) +1
      24. (h, h) |-
      25. = (3*2) +1
      26. (arithmetic) |-
      27. = 6+1
      28. (arthmetic) |-
      29. = 7.

      (End of Net)

      Laboratory 4

      This is to review the idea of the WHILE language. Here is a working C++ program that reads a single positive non-zero number and outputs a pretty random series of numbers. [ 04.cpp ]

      DON'T try to figure it out! I chose a useless program with a well known unpredictable calculation.

      Your task is to remove all control structures except while loops. NO ifs, do-whiles, GOTOs, switches, ... No (_?_:_) are allowed. Assignments, conditions, expressions, input and output are ok. Your version must produce precisely the same results as the original.

      Be ready to show me your code and demonstrate it before the end of the laboratory today.

      Next

      Study chapter 3 on semantics pages 48 to 64 inclusive. [ 05.html ]

    . . . . . . . . . ( end of section CSCI620 Session 4) <<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