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

[Bruno Dutertre <bruno@csl.sri.com>]

David Coppit wrote:
> Hello all,
> 
> This is a followup to my previous stack question. Suppose I defined a
> predicated subtype of Stack called Nonempty_Stack, in order to define
> the "top" operation on only nonempty stacks.
> 
> Now, later, I have a recursive function called multiple_push_pop:
> 
>   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)
> 
> I have a TCC now to prove that the result of the recursive call to
> multiple_push_pop(push(first_value,s), remaining_values) returns a
> nonempty stack:
> 
>   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)))
> 
> How do I go about proving this?  Attached is the complete .pvs file.
> 

David,

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.

You have to change the type of multiple_push_pop so that
multiple_push_pop(s, value) is known to be non-empty when
s is non-empty. For example:

multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE { u: Stack | equals(u, s) } =
    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)

Then the TCCs should all be provable.

Bruno


> Thanks,
> David