Skip to content
Snippets Groups Projects
Commit 2e267952 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] update oracles

- now uses the right type for a boolean function
parent 2491fba9
No related branches found
No related tags found
No related merge requests found
...@@ -80,13 +80,13 @@ ...@@ -80,13 +80,13 @@
------------------------------------------------------------ ------------------------------------------------------------
[wp:script:allgoals] [wp:script:allgoals]
Goal Post-condition (file split.i, line 55) in 'test_step_peq': Goal Post-condition (file split.i, line 55) in 'test_step_peq':
Assume { (* Pre-condition *) Have: L_LQ = L_LP. } Assume { (* Pre-condition *) Have: (L_LQ=true) <-> (L_LP=true). }
Prove: P_S. Prove: P_S.
------------------------------------------------------------ ------------------------------------------------------------
[wp:script:allgoals] [wp:script:allgoals]
Goal Post-condition (file split.i, line 59) in 'test_step_pneq': Goal Post-condition (file split.i, line 59) in 'test_step_pneq':
Assume { (* Pre-condition *) Have: L_LQ != L_LP. } Assume { (* Pre-condition *) Have: !((L_LQ=true) <-> (L_LP=true)). }
Prove: P_S. Prove: P_S.
------------------------------------------------------------ ------------------------------------------------------------
...@@ -195,13 +195,13 @@ ...@@ -195,13 +195,13 @@
[wp:script:allgoals] [wp:script:allgoals]
Goal Post-condition (file split.i, line 107) in 'test_goal_eq': Goal Post-condition (file split.i, line 107) in 'test_goal_eq':
Assume { (* Pre-condition *) Have: P_S. } Assume { (* Pre-condition *) Have: P_S. }
Prove: L_LQ = L_LP. Prove: (L_LQ=true) <-> (L_LP=true).
------------------------------------------------------------ ------------------------------------------------------------
[wp:script:allgoals] [wp:script:allgoals]
Goal Post-condition (file split.i, line 111) in 'test_goal_neq': Goal Post-condition (file split.i, line 111) in 'test_goal_neq':
Assume { (* Pre-condition *) Have: P_S. } Assume { (* Pre-condition *) Have: P_S. }
Prove: L_LQ != L_LP. Prove: !((L_LQ=true) <-> (L_LP=true)).
------------------------------------------------------------ ------------------------------------------------------------
[wp:script:allgoals] [wp:script:allgoals]
...@@ -330,7 +330,7 @@ ...@@ -330,7 +330,7 @@
typed_test_step_pneq_ensures subgoal: typed_test_step_pneq_ensures subgoal:
Goal Wp.Tactical.typed_test_step_pneq_ensures-0 (generated): Goal Wp.Tactical.typed_test_step_pneq_ensures-0 (generated):
Assume { (* True/False *) When: (L_LQ=true) /\ (L_LP=false). } Assume { (* True/False *) When: (L_LP=false) /\ (L_LQ=true). }
Prove: P_S. Prove: P_S.
------------------------------------------------------------ ------------------------------------------------------------
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment