The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8
stars
2
forks
source link
Replace Type.EffectiveArray and Type.EffectiveRecord #57
A sensible refactoring would be to replace Type.EffectiveArray and Type.EffectiveRecord with a single generic type, Type.Effective<T extends Type>. This would be defined thusly:
interface Type.Effective {
T getReadable();
T getWriteable();
}
The next question is: what is an effective type?
Extraction. An effective type is simply an interface for extracting type information from an otherwise unrestricted mixture of various concrete types. In particular, unions, nest unions, intersections, negations, etc.
Multi-moded. By providing access to both read and write information, an effective type can be used in both situations.
Not a type. An effective type is not actually a type in the true sense of the word; rather it is a mechanism for extracting types.
To generate effective type information, it seems sensible that we might want to define some kind of type extractor interface. This would then allow for different extractors to be used. For example, to support different kinds of types and/or different algorithms for generating the data (e.g. caching, etc).
A sensible refactoring would be to replace
Type.EffectiveArrayandType.EffectiveRecordwith a single generic type,Type.Effective<T extends Type>. This would be defined thusly:The next question is: what is an effective type?
To generate effective type information, it seems sensible that we might want to define some kind of type extractor interface. This would then allow for different extractors to be used. For example, to support different kinds of types and/or different algorithms for generating the data (e.g. caching, etc).