[SystemSafety] systemsafety Digest, Vol 75, Issue 24

[Derek M Jones]

Rod,

> That's not quite the way it works in SPARK.  I don't know of any SV tool
> that attempts to analyse "every order of evaluation", since that would
> be (in the worst worst case) O(2**N).

The C-semantics tool evaluates all permutations that could yield
different results: https://github.com/kframework/c-semantics

It is possible to write a program whose number of results forms
a Fibonacci sequence:
http://shape-of-code.coding-guidelines.com/2011/06/18/fibonacci-and-jit-compilers/

It relies on a just-in-time compiler to work, a compile before executing
compiler produces just two possible results.

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com