Skip to content

Commit

Permalink
Set to seq notation and temp scale fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@sakehl
sakehl committed Mar 28, 2024
1 parent 7825896 commit cf315dd
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 30 deletions.
10 changes: 5 additions & 5 deletions examples/concepts/summation/TestCountFail.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@
class TestCount {
public void test_count_E1(){
//@ ghost seq<int> xs = seq<int>{ 1, 2 , 2 , 1 };
//@ assert \sum({ 0 .. 0 },\vcmp(xs,\vrep(1))) == 0;
//@ assert \sum({ 0 .. 1 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum({ 0 .. 2 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum({ 0 .. 3 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum({ 0 .. 4 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 0 ],\vcmp(xs,\vrep(1))) == 0;
//@ assert \sum([ 0 .. 1 ],\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 2 ],\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 3 ],\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 4 ],\vcmp(xs,\vrep(1))) == 1;
}
}

14 changes: 7 additions & 7 deletions examples/concepts/summation/TestCountPass.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,13 @@ class TestCount {
** (vals.size==array.length)
** (\forall int i ; 0 <= i && i < array.length ; array[i]== vals[i])
;
ensures \result == \sum({0 .. array.length},\vcmp(vals,\vrep(3)));
ensures \result == \sum([0 .. array.length],\vcmp(vals,\vrep(3)));
@*/
public int test_count_1(int array[]){
int res=0;
int k=0;
//@ loop_invariant 0 <= k && k <= array.length;
//@ loop_invariant res == \sum({0 .. k},\vcmp(vals,\vrep(3)));
//@ loop_invariant res == \sum([0 .. k],\vcmp(vals,\vrep(3)));
while(k<array.length){
if (array[k]==3){
res = res + 1;
Expand All @@ -29,11 +29,11 @@ public int test_count_1(int array[]){

public void test_count_2(){
//@ ghost seq<int> xs = seq<int>{ 1, 2 , 2 , 3 };
//@ assert \sum({ 0 .. 0 },\vcmp(xs,\vrep(1))) == 0;
//@ assert \sum({ 0 .. 1 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum({ 0 .. 2 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum({ 0 .. 3 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum({ 0 .. 4 },\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 0 ],\vcmp(xs,\vrep(1))) == 0;
//@ assert \sum([ 0 .. 1 ],\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 2 ],\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 3 ],\vcmp(xs,\vrep(1))) == 1;
//@ assert \sum([ 0 .. 4 ],\vcmp(xs,\vrep(1))) == 1;
}

}
Expand Down
26 changes: 13 additions & 13 deletions examples/concepts/summation/TestFloat.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,28 +18,28 @@ public static void main(String args[]){
/*@
ghost seq<float> s=seq<float>{};
assert \sum({0 .. 0},s)==((float)0);
assert \sum([0 .. 0],s)==((float)0);
ghost seq<seq<float>> M=seq<seq<float>>{seq<float>{(float)1}};
assert \sum({0 .. 0}, M[0] ) == ((float)0);
assert \sum({0 .. 1}, M[0] ) == ((float)1);
assert \msum({0 .. 0} * {0 .. 1},M) == ((float)0);
assert \msum({0 .. 1} * {0 .. 1},M) == ((float)1);
assert \sum([0 .. 0], M[0] ) == ((float)0);
assert \sum([0 .. 1], M[0] ) == ((float)1);
assert \msum([0 .. 0] * [0 .. 1],M) == ((float)0);
assert \msum([0 .. 1] * [0 .. 1],M) == ((float)1);
*/
}

/*@
given seq<float> vals;
context_everywhere a!=null ** (a.length == |vals|);
context_everywhere (\forall* int i; 0 <= i && i < a.length;PointsTo(a[i],1\2,vals[i]));
ensures \result == \sum({0 .. a.length},vals);
ensures \result == \sum([0 .. a.length],vals);
@*/
public float add(float a[]){
int k=0;
float res=(float)0;
//@ loop_invariant 0 <= k && k <= a.length;
//@ loop_invariant \sum(({0 ..k}),vals) == res;
//@ loop_invariant \sum(([0 ..k]),vals) == res;
while(k<a.length){
res=res+a[k];
k=k+1;
Expand All @@ -53,14 +53,14 @@ public float add(float a[]){
context_everywhere b!=null ** (a.length == b.length);
context_everywhere (\forall* int i; 0 <= i && i < a.length;PointsTo(a[i],1\2,vals[i]));
context_everywhere (\forall* int i; 0 <= i && i < a.length;Perm(b[i],1));
ensures (\forall int i ; 0 <= i && i < b.length ; b[i] == \sum({0 ..i},vals));
ensures (\forall int i ; 0 <= i && i < b.length ; b[i] == \sum([0 ..i],vals));
@*/
public void prefixsum(float a[],float b[]){
int k=0;
float res=(float)0;
//@ loop_invariant 0 <= k && k <= a.length;
//@ loop_invariant \sum({0 ..k},vals) == res;
//@ loop_invariant (\forall int i ; 0 <= i && i < k ; b[i] == \sum({0 ..i},vals));
//@ loop_invariant \sum([0 ..k],vals) == res;
//@ loop_invariant (\forall int i ; 0 <= i && i < k ; b[i] == \sum([0 ..i],vals));
while(k<a.length){
b[k]=res;
res=res+a[k];
Expand All @@ -74,14 +74,14 @@ public void prefixsum(float a[],float b[]){
context_everywhere b!=null ** (a.length == b.length);
context_everywhere (\forall* int i; 0 <= i && i < a.length;PointsTo(a[i],1\2,vals[i]));
context_everywhere (\forall* int i; 0 <= i && i < a.length;Perm(b[i],1));
ensures (\forall int i ; 0 <= i && i < b.length ; b[i] == \sum({0 ..i},vals));
ensures (\forall int i ; 0 <= i && i < b.length ; b[i] == \sum([0 ..i],vals));
@*/
public void prefixisum(int a[],int b[]){
int k=0;
int res=0;
//@ loop_invariant 0 <= k && k <= a.length;
//@ loop_invariant \sum({0 ..k},vals) == res;
//@ loop_invariant (\forall int i ; 0 <= i && i < k ; b[i] == \sum({0 ..i},vals));
//@ loop_invariant \sum([0 ..k],vals) == res;
//@ loop_invariant (\forall int i ; 0 <= i && i < k ; b[i] == \sum([0 ..i],vals));
while(k<a.length){
b[k]=res;
res=res+a[k];
Expand Down
6 changes: 3 additions & 3 deletions examples/concepts/summation/TestHist.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ class Testhist {
context_everywhere (\forall int i; 0 <= i && i < a.length ; 0 <= a[i] && a[i] < hist.length);
context_everywhere (\forall int i; 0 <= i && i < a.length ; a[i] == vals[i] );
ensures (\forall int i; 0 <= i && i < hist.length ;
hist[i]==\sum({0 .. a.length},\vcmp(vals,\vrep(i))));
hist[i]==\sum([0 .. a.length],\vcmp(vals,\vrep(i))));
@*/
public void histogram(int a[],int hist[]){
int k=0;
//@ loop_invariant 0 <= k && k <= hist.length;
/*@ loop_invariant (\forall int i; 0 <= i && i < k ;
hist[i]==\sum({0 .. 0},\vcmp(vals,\vrep(i))) );
hist[i]==\sum([0 .. 0],\vcmp(vals,\vrep(i))) );
*/
while(k<hist.length){
hist[k]=0;
Expand All @@ -28,7 +28,7 @@ public void histogram(int a[],int hist[]){
k=0;
//@ loop_invariant 0 <= k && k <= a.length;
/*@ loop_invariant (\forall int i; 0 <= i && i < hist.length ;
hist[i]==\sum({0 .. k},\vcmp(vals,\vrep(i))) ); @*/
hist[i]==\sum([0 .. k],\vcmp(vals,\vrep(i))) ); @*/
while(k<a.length){
int v=a[k];
hist[v]++;
Expand Down
6 changes: 4 additions & 2 deletions src/rewrite/vct/rewrite/ResolveScale.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,16 @@ case class ResolveScale[Pre <: Generation]() extends Rewriter[Pre] {

val v = new Variable[Post](TRational())(CheckScale("amount"))

globalDeclarations.declare(function[Post](
globalDeclarations.declare(withResult((result: Result[Post]) => {
function[Post](
blame = PanicBlame("scale ensures nothing"),
contractBlame = PanicBlame("scale only requires a positive rational"),
args = Seq(v),
returnType = TRational(),
body = Some(v.get),
requires = UnitAccountedPredicate(v.get >= const(0)),
)(CheckScale("scale")))
ensures = UnitAccountedPredicate(result >= const(0)),
)(CheckScale("scale"))}))
}

def scaleValue(e: Scale[Pre]): Expr[Post] =
Expand Down

0 comments on commit cf315dd

Please sign in to comment.