Homework 1 Solution

1.     Program correctness (40 points, 10 points each)

a) 
Solution1: (Christina Cyr’s solution)
In logic the specification is the

 

In this example, the

 if x >= y then

   max := x

else

   max := y

{max = x or max = y} and {max >= x and max >=y}

To prove it by working backwards using the {Q(E)} x := E {Q (x)}method to find the Weakest Precondition, Pw:
(Reference: http://www.google.com/search?q=cache:www.middlebury.edu/classes/fall97/learn_assertions/weakestprec.html+Hoare+triples,+Weakest+Precondition&hl=ja )

Proof 1a:
{Going with the case where x >=y.}
Inserting (max := x) into [{max = x or max = y} and {max >= x and max >=y}]
Gives [{x = x or x = y} and {x >= x and x >=y}]
Which gives [{true} and {true and x >=y}]
Which gives x >= y.
Which is true when x is the maximum.

Proof 1b:
{Going with the case where ~(x >=y)}
Inserting (max := y) into [{max = x or max = y} and {max >= x and max >=y}]
Gives [{y = x or y = y} and {y >= x and y >=y}]
Which gives [{true} and {y >= x and true}]
Which gives y >= x.
Which is true when y is the maximum.

Or from a different perspective (another backwards)….

Proof 2a:
Inserting (x >=y) into [{max = x or max = y} and {max >= x and max >=y}]
gives [{max >= y or max = y} and {max >= y and max >= y}],
which reduces to [{max >= y} and {max >= y}],
which reduces even further to {max >= y},
which is {true}.

Proof 2b:
Inserting the reverse case, ˜̃(x >= y), or rather, (x < y) into [{max = x or max = y} and {max >= x and max >=y}]
Gives [{max = x or max > x} and {max >= x and max > x}]]
Which reduces to [{max >= x } and {max > x}]]
Which reduces to {max > x}
Which is {true}.

Using the method shown at http://www.cs.unc.edu/~stotts/COMP204/senotes/proof3/ite1.html

Pre and (x >=y) = Post
True and (x >=y) <=> {max = x or max = y} and {max >= x and max >=y}
True and (x >=y) <=> See “Proof 1a” above.

Pre and ~(x >=y) = Post
True and ~(x >=y) <=> {max = x or max = y} and {max >= x and max >=y}
True and ~(x >=y) <=> See “Proof 1b” above.

The reason that the program on the slide “Be Careful!” did not satisfy the specification of finding the maximum is because it did not satisfy the case where  y > x and abs(y) < abs (x) or vice versa.  For example, if y = 2 and x = -(11), then abs(y) < abs(x) and in the following predicate from the “Be Careful!” slide the max would erroneously become 11.

 

{true}

   max := abs(x)+abs(y);

{max >= x and max >= y}

 

b) (Christina Cyr’s solution)

Utilizing the following from: http://www.cs.caltech.edu/~cs138/1997-98/138a/notes/iter/iteration_html/IterForHTML.html

How can we prove:

where evaluation of the boolean has no side effects?

We prove:

If the then part of the if statement is executed, holds upon initiation of , and from we know that in this case terminates and holds upon termination. If the else part of the if statement is executed, holds upon initiation of , and from we know that in this case terminates and holds upon termination. So, if the if statement is executed in a state in which holds then the statement terminates and holds upon termination.

 

Working backwards,

 

For the case {x < 0} and {x <> 0}, x:= -x.

Inserting  {x := -x} into the Postcondition {x >= 0}

We get {-x >= 0}

Or rather, x <=0.

Which is true for when (x < 0)

And is true for when (x <> 0).

 

For the case ~{x < 0} and {x <> 0}, x:= x – 1.

Inserting  x := x – 1 into the Postcondition {x >= 0} we get {x-1 >= 0}

Or rather, {x >= 1}

Which can also be written as x > 0

Which can also be written as ~(x <= 0)

Which is true when ~{x < 0} and  {x <> 0}.

 

Working forwards,


For the case {x < 0} and {x <> 0}, x:= -x.

Inserting  {x < 0} and {x <> 0} into {x := -x}

Or rather  {x < 0} into {x := -x}

Gives x:= - (<0)

        = - (negative integer)

        = positive integer

Gives x >= 0.

 

For the case ~{x < 0} and {x <> 0}, x:= x - 1.

Inserting ~{x < 0} and {x <> 0} into {x:= x - 1}

Or rather, {x > 0} into {x:= x - 1}

Gives x > 0 -1

      X > -1

             X >= 0. 

 

 

c)  (Tim Williams’s solution)

Prove:

{ y > 0}

               z:= x;

               n:= y;

               while n > 1 do

                              z := z + x;

                              n := n – 1;

               end

{ z = x * y}

 

Scattering intermediate assertions as appropriate (using various algebraic rules to rewrite things), and using the loop invariant

((1 =< n <= y) AND (z = x * (y – n + 1)))

we get

 

{ y > 0}

               z:= x;

{ 1 <= y  AND z = x * 1}

               n:= y;

{ (y = n) AND ((1 =< n <= y) AND (z = x * (y – n + 1)))

               while n > 1 do

{ (1 < n) AND (1 <= n <= y) AND (z = x * (y – n + 1) )

                              z := z + x;

{ (1 < n <= y) AND (z = x * (y – n + 1) + x) }

                              which is the same as

{ (1 <= n <= y) AND (z = x * (y – n + 1 + 1)) }

                              n := n – 1;

                                             back to the loop invariant

{ (1 <= n <= y) AND (z = (y – n  + 1) * x) }

               end

{ n < = 1 AND (1 <= n <= y) AND (z = x * (y – n  + 1)) }

                              which is the same as

{ (1 = n <= y) AND (z = x * (y – 1  + 1)) }

                              which is the same as

{ (1 = n <= y) AND z = (x * y) }

                              which implies the condition

{ z = x * y}

 

 

d)
precondition:        { A <> 0 }  //since in problem it is specified that it is quadratic equation

 

postcondition:

 { ((Ax12 + Bx1 + C = 0) ^ (Ax22 + Bx2 + C = 0) ^ x1 <> x2  ^ B*B-4AC<>0) V

    ((Ax12 + Bx1 + C = 0) ^ (Ax22 + Bx2 + C = 0) ^ x1 = x2  ^ B*B-4AC=0) }

or

postcondition:

      {(x1 = (-B + sqrt(B*B – 4AC))/2A) ^ (x2 = (-B - sqrt(B*B – 4AC))/2A) ^ (B*B-4AC>=0) }

 

Note: The first specification could allow imaginary roots or real roots. The second one only allow real roots.

 

2.      Z

a). (Niniane Wang’s solution)
In the original line

(birthday' = birthday È {name? |® date?)

we know that birthday' is the union of birthday' with the new entry.  In other words, we have added the new entry and made no other modifications to the birthday set. 

 

In the revised case,

{name? |®date?} Î birthday'

we know that the new entry now exists in birthday', but we have no guarantee on other possible modifications to the birthday function. 

 

For example, some programs which would fail the original specification but pass the revised one:

- a program which adds the new entry multiple times

- a program which adds the new entry, and also adds other entries

- a program which adds the new entry and deletes old entries

- a program which does a combination of the above

 

b)      

Solution 1(Scott Jeffus’s solution)

Supplying a year or day construct is making too strong a decision (e.g., consider Unix), so I have come up with the following:

 

---Date----------

| d: DATE

| GetCardinal: DATE -|--> N [where N is the set of natural numbers, and for all d, if d1 describes an earlier DATE than d2, then GetCardinal(d1) < GetCardinal(d2)]

| ----------

| ----------

 

The idea is that one can take any DATE element and map it into a unique natural number such that if the natural number for DATE d1 is n, then the natural number for (d1+1) is n+1. With this type of device, one could define operations for distinguishing earlier and later dates and could compute the difference between any two given dates.

Solution 2 (Sabra A. Wieditz’s solution)

// Definition of Date

__Date__________________

day, month, year: Z

_______________________

               0 < day < 32

               0 < month < 13

________________________

 

// Return Values

BOOL: true | false

// Date1 > Date2

__StrictlyGreater__________

D1?: Date

D2?: Date

Result! : BOOL

________________________

( D1.year > D2.year ^ Result!= true ) Ú

( D1.month > D2.month ^

  D1.year == D2.year ^ Result!= true ) Ú

( D1.day > D2.day ^

  D1.month == D2.month ^

  D1.year == D2.year ^ Result!= true ) Ú

Result!=false

________________________

 

// Date1 == Date2

__Equal_____________

D1?: Date

D2?: Date

Result! : BOOL

________________________

 ( D1.day == D2.day ^

  D1.month == D2.month ^

  D1.year == D2.year ^ Result!= true ) Ú

Result!=false
______________________

 

b)  (Tim Williams’s solution)

i) This first schema describes the state space.  We’re tracking two sets of students, enrolled and completed, where enrolled is all students enrolled in a class and completed is all students who have completed their homework.  We further state that completed is a subset of enrolled (doesn’t make any sense to have a student who isn’t enrolled in the class listed as having completed homework)

+--Register-----

| enrolled : P STUDENT

| completed : P STUDENT

+-----------

| completed Í enrolled

+-----------

 

Initialize the two sets as empty.

+--InitRegister-----

| Register

+------------------

| enrolled = Æ

| completed = Æ

+-------------------

 

ii) Enroll a student.  Add them to the enrolled list, and leave the completed list alone.  Note that we don’t need to check about re-enrolling a student.  Sets are unordered and don’t hold duplicates, so it doesn’t matter if you do re-enroll someone.  This has no error states, assuming that pupil? is indeed of type STUDENT.

+--Enroll-----------

| D Register

| pupil? : STUDENT

+-----------

| enrolled’ = enrolled È {pupil?}

| completed’ = completed

+----------------

 

 

iii) Record a student who must be enrolled as having completed homework.  Again, that we don’t need to check about re-recording a student as completed due to the nature of sets.  However, this schema breaks down in the presence of a student who is not already enrolled, hence it is not robust.

+--Record-----------

| D Register

| pupil? : STUDENT

+-----------

| ((pupil? Î enrolled) Ù

|  enrolled’ = enrolled  Ù

|  completed’ = completed È {pupil?})

+----------------

 

 

iv) The following schemas allow one to enquire whether a student (who must be enrolled) has finished the homework.  We want to give a Yes/No answer, so we first define a data type for Yes and No.

YES_NO ::= Yes | No

 

Now, we check for membership of the pupil in the appropriate sets.  This schema breaks down in the presence of a student who is not already enrolled, so it is not robust.

 

+--HasFinished-----------

| º Register

| pupil? : STUDENT

| finished! : YES_NO

+-----------

| ((pupil? Îenrolled) Ù

|  ((pupil Î completed  Ù finished! = Yes) Ú

|   (pupil Ï completed  Ù finished! = No)     )

+----------------

 

v) To make the system robust, we have to handle some cases where an operation only works if the student is already enrolled.  We start by defining a result to handle either success or the single error case.

REPORT ::== ok | not_enrolled

 

+--Success---------

| result! : REPORT

+------------------

| result! = ok

+------------------

 

+--NotEnrolled----

| º Register

| pupil? : STUDENT

| result! : REPORT

+-----------

| pupil? Ïenrolled

| result! = not_enrolled

+----------------

 

Now, we define a robust version of the system by combining these schemas.  Due to insufficient fonts, I will use the symbol @  to mean set combination (see the Z manual, page 8, for an example of what I mean).  Note that as mentioned in ii) above, there is no error such as AlreadyEnrolled.

 

REnroll @ (Enroll Ù Success)

RRecord @ (Record Ù Success) Ú NotEnrolled

RHasFinished @ (HasFinished Ù Success) Ú NotEnrolled

 

 

vi) To add the restriction that the size of the class can’t be greater than MAX, we first extend the REPORT data type to handle the new report that will be generated if an enrollment can’t be done because of the restriction.

 

REPORT ::== ok | not_enrolled | class_full

 

Now, write a schema that holds MAX.

+--Maximum-----

| MAX : N1

+-----------

+-----------

 

And, create a state space that holds both Register and Maximum.

RegisterMax @ (Register Ù Maximum)

 

Now, write a schema to check for the class being full.  This returns the error class_full if appropriate.  |A| is read as “the cardinality of set A” and is equal to the number of elements in the set A.  Note that this schema works on the state space of RegisterMax, giving it access to both MAX (from Maximum) and enrolled (from Register).

 

+--ClassFull----

| º RegisterMax

| result! : REPORT

+-----------

| MAX < |enrolled|

| result! = class_full

+----------------

 

And, one to check for the class not being full, which returns success if that condition is true.

+--ClassNotFull----

| º RegisterMax

| result! : REPORT

+-----------

| MAX >= |enrolled|

| result! = success

+----------------

 

Now, redefine the robust version of Enroll to check for these cases

REnrollMax @ (Enroll Ù ClassNotFull) Ú ClassFull

And, since MAX has nothing to do with Record or HasFinished, just pick up the already defined robust versions of these

RRecordMax @  RrecordMax

RHasFinishedMax @ RHasFinished

 

Note: I have to admit that I’m not sure whether this limits the size of the class to MAX or (MAX + 1).  I believe it does, since ClassNotFull and Enroll must be satisfied simultaneously, so I think that it checks the size of the set effectively AFTER the student has been enrolled.  Of course, if I rewrote Enroll, I would know for sure because I could check enrolled or enrolled’ as appropriate, but I’m trying to avoid rewriting that schema.

 

 

To be picky, we also need to define InitMaximum to set MAX to some value.  Since no requirement has been set, I can’t actually write this.  Howerver, it would look like this if the maximum was 35.

 

+--InitMaximum-----

| Maximum

+------------------

| MAX = 35

+-------------------

 

And

InitRegisterMax @ (InitRegister Ù InitMaximum)

 

 

 

 

 

 

 

3.     Finite state specifications

Solution1: (Nate Baum’s solution)

After reading the statechart whitepaper by B.P. Douglass and looking at the Yahoo! Checkers site, the most reasonable way to representation the game in a statechart specification is to describe the three frames in the main checkers window as three concurrent states.  The reason I chose to describe the main window in this way is because each area (player list, tables, and chat) changes concurrently with the other two states and change independently from one another.  

 

There are a few areas in this specification that I treated as black box.  For instance the 'Learn More' options, the player profile state, and the states that are occupied while actually playing the game.  I also left out a few of the options to try to stay within reason (and so that I don't go insane).  These options include 'invite' and 'sound' in the game state and the 'rated' checkbox.  

4A.  3 properties in the checkers spec

 

I have come up with a few brief properties that I feel should be part of the spec and can be tested using model checking.  First, I would like to check that the chat state message count property is zero upon first entering the game room.  Second, I would like to check that when the 'create table' event occurs, that the specification enters the hosted game state and the host game property is true.   Third, I would like to check that when the 'Watch' event occurs, the spec enters the watch game state for the appropriate game and the watch game property is true.  

 

 

 

Solution 2: (Dean , Campbell’s solution)

 


4a.  I propose these are properties I would want the specification to exhibit.