Skip to content

EMV2 doesn't check legality of type products #1222

@AaronGreenhouse

Description

@AaronGreenhouse

The legality of type products is not checked. Consider:

package testing
public
	annex EMV2 {**
		error types
			flintstone : type;
			fred : type extends flintstone;
			wilma : type extends flintstone;
			pebbles: type extends flintstone;
			
			rubble : type;
			barney : type extends rubble;
			betty : type extends rubble;
			bambam : type extends rubble;
			
			s1 : type set { fred, wilma } ;
			s2 : type set { barney, s1 };
			s3 : type set { flintstone * rubble };
			s4 : type set { fred * barney, fred * barney }; -- bad
			s5 : type set { fred * wilma }; -- bad
		end types ;
	**};
end testing;

In type set s5, the product fred * wilma should be flagged with an error because fred and wilma are in the same type hierarchy.

Section E.5 paragraph (18) says

Note that different elements of an error type product cannot be from the same type hierarchy.

Furthermore, type set s4 is erroneous because the type type products it contains are not disjoint. That is, it violates Section E.5 paragraph (L7):

If two elements of an error type set are error type products with the same number of
element types and whose element types are from the same type hierarchies, then the
element type of one must not be a subtype of the
other.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions