--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] PVS TCC problem



You're right this is a bug in the printer for PVS. It definitely should
translate any Why3 type into TYPE+. Thanks for noticing and reporting,
this will be fixed asap.

- Claude

On 09/13/2013 11:32 AM, Dragan wrote:
> Hi all,
>  
> I have tried to discharge PVS theorem(s) and obligation generated by
> frama-c-Oxygen -> why2/jessie -> why3 -> PVS using simple example
> written in c language.
> *void swap( int *a , int *b)*
> *{*
> *  int tmp = *a;*
> *  *a = *b;*
> *  *b = tmp;*
> *  return;*
> *}*
> *
> *
> */*@ requires \valid(a) &&  \valid(b);*
> *  @ ensures A: *a==\old(*b); *
> *  @ ensures B: *b==\old(*a);*
> *  @ assigns *a,*b;*
> *  @*/*
> * *
> *void swap( int *a, int *b );*
> 
> There is something interesting I found in *jessie->PVS transformation
> and* I think this is important to report.
> I have successfully proved
> theorem  *wp_parameter_swap_ensures_default *generated automatically.
> However I cannot discharge TCC:
> *select_TCC1[t: TYPE, v: TYPE]: OBLIGATION*
> *  EXISTS (x2: [[memory[t, v], pointer[t]] -> v]): TRUE;*
> All axioms provided above definition  
> *select[t: TYPE, v: TYPE](x: memory[t, v], x1: pointer[t]): v*
> seemed to me are not suitable for discharging this obligation.
> Then I have contacted Sam Owre and we agreed with the following:
> The problem is that as it stands, the TCC is actually false.
> This is because v is a simple type parameter that can be instantiated to
> any type, including an empty one, whereas the argument types for select
> are guaranteed to be nonempty.  
> The easiest fix if this was a manually written spec is to change
> the declaration for select to
> 
> select[t: TYPE, v: TYPE+](x: memory[t, v], x1: pointer[t]): v
>                        ^
>      Note the *'+'* here !
> 
> (or perhaps change memory to be empty if v is and nonempty otherwise,
> but this is probably more difficult).  I think what is going on
> here is that* Why2/jessie-Why3  assumes all types to be nonempty,
> whereas PVS
> doesn't share that assumption. *
> 
> When I added that* '+'* myself, I got no TCCs.
> Please find attached tar.gz ( notice that example
> contain *int* and *real* lib (provided by *Why3*) included as well ).
> 
> Another important thing :
> There are several problems I found during installation  why3 and PVS.
> So I am going to write installation note with all corrections that needs
> to be done.
> 
> Regards
> 
> -- 
> Dragan Stosic
> Senior developer at IBM
> phone: 085-773-1050
> e-mail: dragan.stosic at gmail.com <mailto:dragan.stosic at gmail.com>
> e-mail:DRAGANST at ie.ibm.com <mailto:e-mail%3ADRAGANST at ie.ibm.com>
> IBM Technology Campus
> Damastown Industrial Estate
> Mulhuddart
> Dublin 15
> Ireland
> 
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>