--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] nondeterminism



Does anyone know if Frama-C+Jessie or WP has been used to prove things about a program with nondeterministic choices, like

choose {
  when (guard1) -> do this;
  when (guard2) -> do that;
  ...
}

which means, choose one of the clauses for which the guard evaluates to true and execute that statement.

I guess you could obtain something like this using a function "chooseBool()" which returns a boolean and which is totally unconstrained, and use that as the condition in an "if" statement.  Or you could use a function "chooseInt()" with a switch statement.

Just wondering if anyone has done anything like that,

Thanks,
Steve