Menu

#186 Dependent witnesses

V0.8.1
closed
5
2008-02-27
2008-02-13
Anonymous
No

Hi all,

let's say you have an event with two variables:
e = ANY a,b WHERE ...

and you want to refine to an event without those variables:
e = ANY c WHERE ...

then is not possible inside the witness of a to use the variable b (and vice versa).
error msg: "identifier b has not been declared"

It's very annoying if one want to really use the refinement.

I attach a archive as example.

see you soon

Discussion

  • Nobody/Anonymous

     
  • Laurent Voisin

    Laurent Voisin - 2008-02-19
    • labels: --> Event-B static checker
    • milestone: --> V0.8.1
    • assigned_to: nobody --> halstefa
     
  • Stefan Hallerstede

    • status: open --> closed
     
  • Stefan Hallerstede

    Logged In: YES
    user_id=1371449
    Originator: NO

    This is not a bug. Mentioning b would be formally wrong. One-point rule! However, I agree that a generalisation of the witnesses as currently implemented would be very useful. We are working on this - the price will be an extra proof obligation to guarantee the existence of such generalised witnesses.

     

Log in to post a comment.