New Feature Request -- Inheritance Support

[kfhoech]

Issue by bulletshot60 Thursday Jun 04, 2015 at 13:41 GMT Originally opened as https://github.com/smaccm/smaccm/issues/39

---

I am raising an issue to discuss the possibility of the inclusion of a new feature in AGREE. I would like to see better support for the use of the "extends" concept in AADL, and my idea is the inclusion of an abstract local variable. An example prototype of what I am thinking follows below.

package Sample
public
    system A
        features
            input: in data port;
            output: out data port;
        annex agree {**
            assume "we won't divide by 0 or a non-negative": input >= 1;
            guarantee "we will produce a non-negative value": output >= 0;
        **};
    end A;

    system implementation A.impl
        annex agree {**
            eq abstract out: int;
            assert output = out;
        **};
        --attempting to verify this system will verify its ultimate non-abstract extensions (D and C)
        --since this system cannot be verified due to the abstract
    end A.impl;

    system B extends A
        annex agree {**
            --these are automatically added from A due to the extension
            --assume "we won't divide by 0 or a non-negative" input >= 1;
            --guarantee "we will produce a non-negative value": output >= 0;
            guarantee "output = 2048 / input": output = 2048 / input;               
        **};
    end B;

    system implementation B.impl extends A.impl
        annex agree {**
            --these are automatically added from A due to extension
            --eq abstract out: int;
            --assert output = out;
            eq abstract out2: int;
        **};
    end B.impl;

    system C extends A
        annex agree {**
            --these are automatically added from A due to the extension
            --assume "we won't divide by 0 or a non-negative" input >= 1;
            --guarantee "we will produce a non-negative value": output >= 0;
            guarantee "output = 2048 / input": output = 2048 / input;
        **};
    end C;

    system implementation C.impl
        annex agree {**
            --these are automatically added from A due to extension
            --eq abstract out: int;
            --assert output = out;
            eq out: int = 2048 / input;
        **};
    end C.impl;

    system D extends B
        annex agree {**
            --these are automatically added from B due to the extension
            --assume "we won't divide by 0 or a non-negative" input >= 1;
            --guarantee "we will produce a non-negative value": output >= 0;
            --guarantee "output = 2048 / input": output = 2048 / input;             
        **};
    end D;

    system implementation D.impl extends B.impl
        annex agree {**
            --these are automatically added from B due to extension
            --eq abstract out: int;
            --assert output = out;
            --eq abstract out2: int;
            --validation error, must have same type as defining abstract (int)
            eq out2: bool = false;
            assert output = out2;
            --validation error, abstract out must be defined
        **};
    end D.impl;
end Sample;

The approach above uses a copy-down approach where extensions of a component copy down the contracts of their parents. Abstract variables must be ultimately given a definition, it would be invalid for an abstract to remain undefined at one of the leaf nodes of the inheritance hierarchy, although its definition could be given higher in the tree (in the example above out defined in B leaving it invalid for it to also be defined in D).

The abstract variable would make it impossible to verify a system, so in the event an AGREE annex has an abstract, the extensions of the component would be verified in place of the abstract component. Or to prevent state explosion, the abstract component is simply assumed to be correct, and the abstract is only ever verified if one extensions of the abstract is verified. Either approach would be sufficient in my thinking.

Thank you for your consideration. Thoughts / Questions?

[kfhoech]

Comment by backesj Tuesday Jun 16, 2015 at 13:40 GMT

---

Hi Ethan,

Sorry I thought I responded to this a while back. The email was in my drafts folder and I never sent it :-(.

I'm confused about the comments in this component:

system implementation B.impl annex agree { --these are automatically added from A due to extension --eq abstract out: int; --assert output = out; eq abstract out2: int; }; end B.impl;

How does the implementation of "B.impl" know to reference the syntax in in the annex of "A.impl"? The extends clause in the component type definition for B only references the component type of A (not the implementation A.impl). Because there can be many implementations for a single type it doesn't make sense to me that an implementation of a component defined with an extends clause would inherit syntax in some implementation of the extended type. Let me know if I didn't articulate this well, I can explain more if this is confusing.

As for inheritence for component types, I think the idea seems okay. It does however make it easier for a user to specify inconsistent/unrealizable contracts.

• John

On Thu, Jun 4, 2015 at 8:41 AM, Ethan McGee notifications@github.com wrote:

I am raising an issue to discuss the possibility of the inclusion of a new feature in AGREE. I would like to see better support for the use of the "extends" concept in AADL, and my idea is the inclusion of an abstract local variable. An example prototype of what I am thinking follows below.

package Sample public system A features input: in data port; output: out data port; annex agree { assume "we won't divide by 0 or a non-negative" input >= 1; guarantee "we will produce a non-negative value": output >= 0; }; end A;

system implementation A.impl
    annex agree {**
        eq abstract out: int;
        assert output = out;
    **};
    --attempting to verify this system will verify its ultimate non-abstract extensions (D and C)
    --since this system cannot be verified due to the abstract
end A.impl;

system B extends A
    annex agree {**
        --these are automatically added from A due to the extension
        --assume "we won't divide by 0 or a non-negative" input >= 1;
        --guarantee "we will produce a non-negative value": output >= 0;
        guarantee "output = 2048 / input": output = 2048 / input;
    **};
end B;

system implementation B.impl
    annex agree {**
        --these are automatically added from A due to extension
        --eq abstract out: int;
        --assert output = out;
        eq abstract out2: int;
    **};
end B.impl;

system C extends A
    annex agree {**
        --these are automatically added from A due to the extension
        --assume "we won't divide by 0 or a non-negative" input >= 1;
        --guarantee "we will produce a non-negative value": output >= 0;
        guarantee "output = 2048 / input": output = 2048 / input;
    **};
end C;

system implementation C.impl
    annex agree {**
        --these are automatically added from A due to extension
        --eq abstract out: int;
        --assert output = out;
        eq out: int = 2048 / input;
    **};
end C.impl;

system D extends B
    annex agree {**
        --these are automatically added from B due to the extension
        --assume "we won't divide by 0 or a non-negative" input >= 1;
        --guarantee "we will produce a non-negative value": output >= 0;
        --guarantee "output = 2048 / input": output = 2048 / input;
    **};
end D;

system implementation D.impl
    annex agree {**
        --these are automatically added from B due to extension
        --eq abstract out: int;
        --assert output = out;
        --eq abstract out2: int;
        --validation error, must have same type as defining abstract (int)
        eq out2: bool = false;
        assert output = out2;
        --validation error, abstract out must be defined
    **};
end D.impl;

end Sample;

The approach above uses a copy-down approach where extensions of a component copy down the contracts of their parents. Abstract variables must be ultimately given a definition, it would be invalid for an abstract to remain undefined at one of the leaf nodes of the inheritance hierarchy, although its definition could be given higher in the tree (in the example above out defined in B leaving it invalid for it to also be defined in D).

The abstract variable would make it impossible to verify a system, so in the event an AGREE annex has an abstract, the extensions of the component would be verified in place of the abstract component. Or to prevent state explosion, the abstract component is simply assumed to be correct, and the abstract is only ever verified if one extensions of the abstract is verified. Either approach would be sufficient in my thinking.

Thank you for your consideration. Thoughts / Questions?

— Reply to this email directly or view it on GitHub https://github.com/smaccm/smaccm/issues/39.

[kfhoech]

Comment by bulletshot60 Tuesday Jun 16, 2015 at 13:53 GMT

---

You're correct. I had forgotten to have B.impl extend A.impl as well as B extend A. It would not make sense the way my example was initially. My apologies for the confusion caused. I have corrected the initial example.

The use case I had in mind for this was to have a mostly realized parent with one or two abstract variables defined that the children, whose behavior varies in only minor ways, would implement. I can accomplish the same thing by copy / pasting from the parent to the children, but that makes changing the AGREE contracts more difficult since I have to do it in multiple places. It would just be nice if there was a syntactical method for handling this sort of problem so I figured why not make a request.

[kfhoech]

Comment by backesj Tuesday Jun 16, 2015 at 14:04 GMT

---

I think this makes sense.

My biggest concern is if you have some guarantee like this in the parent:

guarantee "x is true" : x;

and then a guarantee like this in the component that extends the parent:

guarantee "x is not true": not x;

This would make the model inconsistent, and it could be very difficult to track down. I guess the best way around this would be to do a consistency check on both the parent and the component that extends the parent. This would require a bit of work. I can probably implement this eventually, but it's not a big priority right now. Unless a bunch of users request this feature. If you wanted to go ahead and implement it I would be happy to pull it in the main branch :-)

• John

On Tue, Jun 16, 2015 at 8:53 AM, Ethan McGee notifications@github.com wrote:

You're correct. I had forgotten to have B.impl extend A.impl as well as B extend A. It would not make sense the way my example was initially. My apologies for the confusion caused.

The use case I had in mind for this was to have a mostly realized parent with one or two abstract variables defined that the children, whose behavior varies in only minor ways, would implement. I can accomplish the same thing by copy / pasting from the parent to the children, but that makes changing the AGREE contracts more difficult since I have to do it in multiple places. It would just be nice if there was a syntactical method for handling this sort of problem so I figured why not make a request.

— Reply to this email directly or view it on GitHub https://github.com/smaccm/smaccm/issues/39#issuecomment-112439562.

[kfhoech]

Comment by bulletshot60 Wednesday Dec 09, 2015 at 04:04 GMT

---

John,

My apologies that development on this took so long. My advisor and I went down another path for a few months and this got sidelined as a result. We finally came back to this issue a few weeks ago and I was able to finish the work. A pull request has been made per your request.

Please let me know of any changes that are needed in order for this to become incorporated into the language.

Thanks!

[kfhoech]

Comment by bulletshot60 Monday May 09, 2016 at 19:09 GMT

---

John,

Just reaching out to see if a decision has been made concerning adding support for inheritance. If any changes are needed in the pull request or further discussion is warranted, please let us know.

Thanks.