--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on September 2013 ---
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