joyheron / eventb_gen Goto Github PK

The eventb_gen tool seems to auto-generate labels inv0, inv1,... There is a type clash in case the user uses the same label himself or herself.

Example:
procedure first_of_str(NullableSet,FirstRel,str) => first_str
sees symbols

typing NullableSet: POW(N)
typing FirstRel: N --> POW(T)
typing str: String
typing first_str: POW(T)

precondition str:String & FirstRel: N --> POW(T) & first_of_str <: T
postcondition first_str <: T & (str[{1}] \ T) <: first_str

implementation
var i type i:NAT1 init i ≔ 1;
var F type F<:T init F := {}
invariants
@INV1 i:1..(card(str)+1)
@Inv2 F <: T

  algorithm
     while: i <= card(str)
        invariant i: 1..card(str)
        variant card(str)+1-i
     do
        if: str(i) : T then
          @term F := F \/ {str(i)}
        else
          @nonterm F := F \/ FirstRel(str(i))
        end;
        if: str(i) : NullableSet then
          @inc i := i+1
        else
          @exit i := card(str)+1
        end
     end; 
     return F
  end

end
end