--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on September 2013 ---
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 >