type error in Alloy -
i have alloy specification represent subset of java programming language. below have part of model:
abstract sig type {} 1 sig void_ extends type {} abstract sig primitivetype extends type {} 1 sig int_, long_ extends primitivetype {} sig method { id : 1 methodid, param: lone type, acc: lone accessibility, return: 1 type, b: 1 body }{ (return=void_) => ( ( (b=constructormethodinvocation) => (b.cmethodinvoked).return = void_) || ( (b=methodinvocation) => ((b.id_methodinvoked).return = void_) ) ) } abstract sig body {} sig methodinvocation extends body { id_methodinvoked : 1 method, q: lone qualifier } sig constructormethodinvocation extends body { id_class : 1 class, cmethodinvoked: 1 method }{ this.@cmethodinvoked.acc != private_ this.@cmethodinvoked in ((this.@id_class).*extend).methods }
in code, there type error in method signature, is:
this cannot legal relational join left hand side . (this/method <: b) . (this/constructormethodinvocation <: cmethodinvoked) (type = {this/method}) right hand side . (this/method <: return) (type = {this/type})
and not understanding why.
thanks in advance,
the problem "return" implicitely scoped , represents result of "this.return", i.e. "return" "type", not relation "method" "type".
a possible solution avoid implicit scoping using separate "fact" section , explicitly quantify on "methods":
fact { m: method | (m.return = void_ ..... }
Comments
Post a Comment