[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] TCC Question (Stack followup)

On Mon, 3 Oct 2005, Bruno Dutertre wrote:

> David Coppit wrote:

>>   multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE Stack =
>>     IF (values = null) THEN
>>       s
>>     ELSE
>>       LET (first_value, remaining_values) = (car(values), cdr(values)) IN
>>         pop(multiple_push_pop(push(first_value,s), remaining_values))
>>     ENDIF
>>   MEASURE length(values)

>>   multiple_push_pop_TCC3 :
>>     |-------
>>   {1}   FORALL (s: Stack, values: list[Value],
>>                 v:
>>                   [{z: [Stack, list[Value]] |
>>                             length(z`2) < length(values)} ->
>>                      Stack]):
>>           NOT (values = null) IMPLIES
>>            (FORALL (first_value: Value, remaining_values: list[Value]):
>>               remaining_values = cdr(values) AND first_value = car(values)
>>                IMPLIES
>>                NOT is_empty?(v(push(first_value, s), remaining_values)))

> You cannot prove this because it's not true. In the above TCC, v is
> an arbitrary function of type [... -> Stack], so nothing guarantees
> that v(push(first_value, s), remaining_values)) is non empty.

But that's the problem I'm having--I agree that it shouldn't be true for
an arbitrary function. But shouldn't it be true for multiple_push_pop?

i.e. Cases:

- values is empty: TCC not applicable since pop() not involved (return
   stack is either nonempty or empty, depending on argument stack s)
- values has 1 element: push(first_value,s) is nonempty, so
   multiple_push_pop(push(first_value,s),null) is nonempty
- values has >1 elements: push(first_value,s) is nonempty, and
   multiple_push_pop(push(first_value,s),null) eventually involves the
   previous nonempty case

It seems to me that PVS has lost the structure of the multiple_push_pop
function that guarantees that in the values /= null case that the result
will be nonempty.

> multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE { u: Stack | 
> equals(u, s) } =

Hm... I would have thought that the equals() bit belongs in a lemma, not
the function definition. It feels like "cheating", like introducing an
axiom to do away a problematic proof step.

I guess I would feel a little better with this:

multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE
   { u: Stack | is_empty?(s) <=> is_empty?(u) } =


David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals