search

Whiley / WhileyTheoremProver

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

Problem of Unresolved Names in TypeInvariantExtractor #134

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following minimal example illustrates a problem with TypeInvariantExtractor:

import std.io

method main():
    io.println("hello world")

The problem is related to the type std.ascii.string which is given as the fully qualified type for "hello world". When expanding the invariant for that type we encounter the element type char. However, this name is brought over from its enclosing WyalFile into the local StructurallyAllocatedHeap and, in this process, the path qualification is lost.

A temporary fix has been patched against v0.6.4 which simply expands all names to their fully qualified equivalents during this process.