search

Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
218 stars 36 forks source link

Sublist Bug? #287

Closed DavePearce closed 11 years ago

DavePearce commented 11 years ago

Currently, the theorem prover does not support the sublist operation. The following test case causes a NullPointerException:

define posintlist as [int] where no { x in $ | x < 0 }

int sum(posintlist ls) ensures $ >= 0:
    if(|ls| == 0):
        return 0
    else:
        rest = ls[1..]
        return ls[0] + sum(rest)
DavePearce commented 11 years ago

This is no longer causing a NullPointerException, but it's also not passing (presumably because list append is not working properly because of axiom instantiation --- see #292).