0

I have an Alloy specification to represent a subset of java programming language. Below we have some part of this model:

  abstract sig Type {}

  one sig void_ extends Type {}

  abstract sig PrimitiveType extends Type {}

  one sig Int_, Long_ extends PrimitiveType {}

  sig Method {
       id : one MethodId,
       param: lone Type,
       acc: lone Accessibility,
       return: one Type,
       b: one 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 : one Method,
        q: lone Qualifier
    }

    sig ConstructorMethodInvocation extends Body {
        id_Class : one Class,
        cmethodInvoked: one Method
    }{
        [email protected] != private_
        this.@cmethodInvoked in ((this.@id_Class).*extend).methods
    }

In this code, there is a type error in Method signature, that is:

This cannot be a legal relational join where
left hand side is this . (this/Method <: b) .
(this/ConstructorMethodInvocation <: cmethodInvoked) (type =
{this/Method})
right hand side is this . (this/Method <: return) (type =
{this/Type})

And i am not understanding why.

Thanks in advance,

1 Answer 1

1

The problem is that "return" is implicitely scoped and thus represents the result of "this.return", i.e. "return" is already a "Type", not a relation from "Method" to "Type".

A possible solution is to avoid the implicit scoping by using a separate "fact" section and explicitly quantify over all "Methods":

fact {
  all m: Method | (m.return = void_ .....
}
3
  • Thank you for the answer, wmeyer, but i do not understand why return is not a relation from "Method", why "return" is implicitely scoped? could you give me more details?
    – Tarciana
    May 19, 2014 at 13:18
  • "return" is implicitly scoped because it is used inside of a signature fact. See Alloy 3.0 Reference Manual (can be found with Google). Quote: "Like any other fact, the signature fact is a constraint that always holds. Unlike other facts, however, a signature fact is implicitly quantified over the signature set. Given the signature declaration sig S {…} { F} the signature fact F is interpreted as if one had written an explicit fact fact{ allthis: S | F’}
    – wmeyer
    May 19, 2014 at 14:06
  • ok, thank you again for the clarification, wmeyer, but what i remain not understanding is: why return (as a valid relation of Method signature) can not be used in a signature fact?
    – Tarciana
    May 20, 2014 at 1:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.