TABLE OF ASSIGNMENTS

  A1*  reading; practice thought problems
  A2*  reading; practice FSM and Pnet problems
  A3*  reading; practice logic specifications
  A4*  reading; Hoare rule for repeat/until


:A1
>Key=B
ASSIGNMENT 01                 assigned: lecture L01*

  READ 

 text Chapter 1 
 text Chapter 2

:A1.1
ASSIGNMENT 01                 assigned: lecture L01*

  PRACTICE 

 a) text Exercises 2.1, 2.2, 2.5 

?Assignments ?Back A1

:A2
>Key=B
ASSIGNMENT 02                 assigned: lecture L02*

  READ

 finite state machines
   text Section 5.5.2 

 Petri nets and case study
   text Section 5.5.3 
   paper Peterson (for more background)
   paper Murata (if very interested)
:A2.1
ASSIGNMENT 02                 assigned: lecture L02*

  PRACTICE

 a) text Exercise 5.7, 5.8, 5.9, 5.10, 5.11, 5.12
 b) Design a Pnet to test if "(" and ")" characters 
    in a string are properly nested and balanced. 
 c) Design a Pnet that implements a 3 stage pipeline,
    that is, one stage feeds into the next, and only
    one activity (token) can be in a stage at a time.
 d) Design a Pnet to model a binary counter that
    counts 0-15.  Explain your interpretation of
    the net (when it's valid to read a number, etc.)
 e) Design a Pnet that has 3 resources, and allows 
    any two resources to be active at a time.  Allow 
    one activity (token) per resource at a time.
?Assignments ?Back A2

:A3
>Key=B
ASSIGNMENT 03                 assigned: lecture L03*

  READ

 predicate calculus
   text Section 5.6.2 

 verification
   text Chapter 6 thru Section 6.1 
   text Section 6.4 especially Section 6.4.2 
:A3.1
ASSIGNMENT 03                 assigned: lecture L03*

  PRACTICE

 a) text Exercise 5.32

 b) Express these properties in predicate calculus:
    - the density of reals
    - the non-density of integers
    - given two arrays, A and B, each element in B 
      is larger than the corresponding element in A
    - given two arrays, A and B, each element in B 
      is larger than all elements in A that have the 
      same index or higher
    - given two integers x and y, x is a multiple 
      of y
    - a natural number z is prime

 c) for this program, express in predicate calculus 
    some loop invariants (there are many):

       y := 0
       while x < 0 do
         y := y + x
         x := x + 1
       end

?Assignments ?Back A3

:A4
>Key=B
ASSIGNMENT 04                 assigned: lecture L04*

  READ

 axiomatic verification
   text Section 6.4.2 thru p. 309

:A4.0
ASSIGNMENT 04                 assigned: lecture L04*

  PRACTICE

 a) generate an inference rule for a 
    repeat/until loop control structure

 b) bubble*
    use your repeat/until rule to verify the 
    inner loop of a bubble sort

?Assignments ?Back A4

:A4.1
:bubble
Inner loop of Bubble Sort

 { a < b }

   i := a
   repeat
     if x[i] > x[i+1] then
       t := x[i]
       x[i] := x[i+1]
       x[i+1] := t
     end
     i := i + 1
   until i = b

 { forall j: a <= j <= b ==> x[b] >= x[j] }

?Back A4.0