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.
The method SyntacticElement.attributes() in the end is not a good idea. This needs to be removed and replaced with an attribute registration mechanism.
I have made some progress towards this via the WyalFileParser.allocate() function. More needs to be done to see it through though. In particular, we need to:
Remove SyntacticElement.attributes() and possible SyntacticElement altogether.
Add a concept of SyntacticAttribute or similar which is basically a reference to a given SyntacticItem which can include additional information, etc.
Add an implement of SyntacticAttribute called Span. This provides the notion of a contiguous portion of a source file (currently equivalent to Attribute.Source.
Add a mechanism for querying a CompilationUnit for extracting the SyntacticAttribute instances associated with a given SyntacticItem.
The method
SyntacticElement.attributes()in the end is not a good idea. This needs to be removed and replaced with an attribute registration mechanism.I have made some progress towards this via the
WyalFileParser.allocate()function. More needs to be done to see it through though. In particular, we need to:SyntacticElement.attributes()and possibleSyntacticElementaltogether.SyntacticAttributeor similar which is basically a reference to a givenSyntacticItemwhich can include additional information, etc.SyntacticAttributecalledSpan. This provides the notion of a contiguous portion of a source file (currently equivalent toAttribute.Source.CompilationUnitfor extracting theSyntacticAttributeinstances associated with a givenSyntacticItem.