WhileyCompiler
WhileyCompiler copied to clipboard
Whiley
The Whiley Compiler (WyC)
There is a problem parsing qualified record initialisers, like so: ```Whiley return st,[ io::Get{url:"/compile",ok:&ok_handler,error:&err_handler} ] ``` Here, `io::Get` is the problem. However, if use imports and rewrite as `Get{url ...}`...
For some reason, the following code from `Conway.wy` generates an error: ```Whiley // Apply click to model state model::State st = model::click(x,y,*pState) // Update state object *pState = st ```...
Currently, we have two types of assignment: _interfering_ and _non-interfering_. The latter could also be referred to as _parallel_ or perhaps _atomic_. The following illustrates: ```Whiley int a = 1...
Does this make sense: ```Whiley method main(int[] xs, int i, int j): xs[i],xs[j]= 0,1 ``` What is the semantics of this? Dafny disallows this.
The purpose of this interface is to help assess memory requirements. It is defined something like this: ```Java interface Sizeable { int sizeOf(); } ``` Various interfaces should implement it,...
_(See also #937)_ The following test (`UnionType_Valid_28`) fails to type check for reasons unknown: ```Whiley type Tree is null | Node type Node is { int data, Tree left, Tree...
At the moment, the following is prohibited: ```Whiley function f(&int p) -> (int r): return *p ``` It says "dereference not permitted". This will need to be corrected.
Test `001137` is as follows: ```Whiley method assign(&T x, &T y, T v1, T v2) ensures *x == v1 ensures *y == v2: // Broken if x == y *x...
_(see also #1145)_ `000497` fails because it attempts to check (at runtime) the invariant of a cyclic type: ```whiley type Cyclic is { null|&Cyclic ptr, int data } public export...
Need to figure this out in conjunction with the standard library.