Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

MRSolver SpecM bugfixes #1952

Merged
merged 9 commits into from
Oct 5, 2023
Prev Previous commit
Next Next commit
update SpecPrims.cry, specPrims.saw to use SpecM
m-yac committed Sep 28, 2023
commit c64822fbfdf4f5af0cfd8eab24ae282e5b1a239b
22 changes: 11 additions & 11 deletions heapster-saw/examples/SpecPrims.cry
Original file line number Diff line number Diff line change
@@ -2,25 +2,25 @@ module SpecPrims where

/* Specification primitives */

// The specification that holds for f x for some input x
exists : {a, b} (a -> b) -> b
exists f = error "Cannot run exists"
// The specification that holds for for some element of type a
m-yac marked this conversation as resolved.
Show resolved Hide resolved
exists : {a} a
exists = error "Cannot run exists"

// The specification that holds for f x for all inputs x
forall : {a, b} (a -> b) -> b
forall f = error "Cannot run forall"
// The specification that holds for for all elements of type a
m-yac marked this conversation as resolved.
Show resolved Hide resolved
forall : {a} a
forall = error "Cannot run forall"

// The specification that a computation returns some value with no errors
returnsSpec : {a} a
returnsSpec = exists (\x -> x)
// The specification that a computation has no errors
noErrors : {a} a
noErrors = exists

// The specification that matches any computation. This calls exists at the
// function type () -> a, which is monadified to () -> CompM a. This means that
// function type () -> a, which is monadified to () -> SpecM a. This means that
// the exists does not just quantify over all values of type a like noErrors,
// but it quantifies over all computations of type a, including those that
// contain errors.
anySpec : {a} a
anySpec = exists (\f -> f ())
anySpec = exists ()

// The specification which asserts that the first argument is True and then
// returns the second argument
11 changes: 5 additions & 6 deletions heapster-saw/examples/specPrims.saw
Original file line number Diff line number Diff line change
@@ -2,9 +2,8 @@

import "SpecPrims.cry";

set_monadification "exists" "Prelude.existsM";
set_monadification "forall" "Prelude.forallM";
set_monadification "anySpec" "Prelude.anySpec";
set_monadification "asserting" "Prelude.asserting";
set_monadification "assuming" "Prelude.assuming";
set_monadification "invariantHint" "Prelude.invariantHint";
set_monadification "exists" "Prelude.existsS" true;
set_monadification "forall" "Prelude.forallS" true;
set_monadification "asserting" "Prelude.asserting" true;
set_monadification "assuming" "Prelude.assuming" true;
set_monadification "invariantHint" "Prelude.invariantHint" true;