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