Re: Assitance - Formal Programming

Thank you for answering my question in the newsgroup (comp.programming).
I am presently reading "The Science of Programming" by David Gries, in
order to gain a better understating of proving programs correct. For the
particular program in question, I was trying to verify using the weakest
pre-condition notation that the first 3 items on his checklist in his
book hold on table 11.9. These are

1. Show that P is true before execution of the loop begins.
2. Show that {P^Bi} Si {P}, for 1<=i<=n. That is, execution of each
guarded command terminates with P true, so that P is indeed an invariant
of the loop.
3. Show that P ^ -BB ==> R, ie upon termination the desired result is
true.

He covers the notation in his book but I am not familiar with writing it
for If statements within a loop. Are you familiar with this technique
and could possible shed some light on this?

Thanks for your help.


Tim Rentsch <txr@xxxxxxxxxxxxxxxxxxx> wrote in
news:kfnr78ult9p.fsf@xxxxxxxxxxxxxxxxxxx:

> "Michael T. Gacek" <mgacek@xxxxxxxxxxxxxxx> writes:
>
>> This is the question: Let b[0:n-1] be a fixed, ordered array with
>> n>0. A plateua of the array is a sequence (of length greater than or
>> equal to 1) of each values. Write an algorithm that finds the number
>> of plateaus in b. The answer should involve writing a postcondition
>> and invariant. Also using WP (weakest precondtion), I want to prove
>> the first three points of the Gries checklist in table 11.9.
>>
>> I have come up with this. Could someone verify it, and possibly
>> figure out how I could assertain the weakest precondition?
>>
>> {0=0}
>> i,p := 1,1
>> {Invariant P: 1<=i<n ^ p is the number of plateus in array b[0:n-1]}
>> do i != n ==> if b[i] = b[i+1] ==> SKIP
>> [] b[i] != b[i+1] p:= p+1
>> fi
>> i=i+1
>> od
>> {R: (p is the number of plateaus in b[0:n-1]}
>
> It's a good attempt. There's a glitch or two. I might write it
> this way (using '==' to mean an equality test):
>
> { 1 <= n }
> i,p := 1,1
> {Invariant Pi: 1 <= i <= n AND p == "number of plateaus in
> b[0:i-1]"} do i != n ==>
>
> if b[i-1] == b[i] ==> i,p := i+1,p
> [] b[i-1] != b[i] ==> i,p := i+1,p+1
> fi
>
> od
> {Pi AND i == n => Pn: p == "number of plateaus in b[0:n-1]"}
>
> Please note the array limits in the invariant Pi. Also,
> the final braced condition is meant to be both a statement
> of the postcondition Pn and a simple implication that shows
> that Pn holds.
>
> The precondition { 1 <= n } needs to be true so that Pi is
> established initially. You should be able to show that
> precondition using the predicate transformer for assignment
> and one part of Pi (namely, i <= n).
>
> Depending on the exact definition of the term "plateau", it
> may also be necessary to include in the initial precondition
> that the array elements are in non-decreasing order. That
> condition isn't needed to establish Pi initially, but it
> might be needed to establish that Pi is maintained by the
> statement in the do...od loop. In particular, if we want to
> conclude that b[i-1] != b[i] implies that b[i] is not equal
> to any previous values of b, then we need to know more than
> just that the array has values in it. The condition of
> the array being ordered would be sufficient for that. Being
> ordered is not the _weakest_ condition to establish that;
> you might try to see if you can figure out the weakest
> precondition needed to establish
>
> b[i-1] != b[i] => "no element of b before b[i] has the
> same value as b[i]"
>
> Good luck!

.

Relevant Pages

  • Re: Puppy Mastiff wants to Nip at Faces
    ... in my first college textbook on structured programming. ... they did was loop through an array to show how you could easily ... design, PIC code, and real time programming. ...
    (rec.pets.dogs.behavior)
  • Re: Puppy Mastiff wants to Nip at Faces
    ... in my first college textbook on structured programming. ... they did was loop through an array to show how you could easily access ...   and improve your crack pot licensing fee calculator. ...
    (rec.pets.dogs.behavior)
  • Re: Puppy Mastiff wants to Nip at Faces
    ... in my first college textbook on structured programming. ... they did was loop through an array to show how you could easily access ...   arrays and loops because it makes for less work. ...
    (rec.pets.dogs.behavior)
  • Re: phrase search
    ... Find shortest array Ps of the Pi's ... What programming languagedo you use? ... Take the pseudo-code, and copy it directly into the source code file. ... Then there's what they call a "for loop", ...
    (sci.logic)
  • Re: Assitance - Formal Programming
    ... weakest pre-conditions in order for those 3 items on the Gries checklist ... Show that P is true before execution of the loop begins. ... >>> figure out how I could assertain the weakest precondition? ... >> that the array elements are in non-decreasing order. ...
    (comp.programming)