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

Popular posts from this blog

how to proxy from https to http with lighttpd -

android - Automated my builds -

python - Flask migration error -