```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

```