Skip to content
This repository has been archived by the owner on Jul 19, 2019. It is now read-only.

Commit

Permalink
updated model
Browse files Browse the repository at this point in the history
  • Loading branch information
Joy Clark committed Dec 13, 2015
1 parent 056536c commit 27e7fba
Showing 1 changed file with 96 additions and 25 deletions.
121 changes: 96 additions & 25 deletions de.prob2.kernel/groovyTests/assertionPropagation.groovy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,43 +9,46 @@ import de.prob.statespace.*
mm = new ModelModifier().make {

context(name: "limits") {
constants "maxInt", "myNAT", "myINT"
constants "MAXINT", "NATURAL", "INTEGER"

axioms "maxInt : NAT",
"myNAT = 0..maxInt",
"myINT = (-maxInt)..maxInt"
axioms "MAXINT : NAT",
"NATURAL = 0..MAXINT",
"INTEGER = (-MAXINT)..MAXINT"
}

context(name: "csts", extends: "limits") {
context(name: "constants_correct", extends: "limits") {
constants "a", "aSize"

axioms "aSize : myNAT",
"a : 0..aSize-1 --> myINT",
"!j,k.j : dom(a) & k : dom(a) & j < k => a(j) < a(k)"
axioms "aSize : NATURAL",
"a : 0..aSize-1 --> INTEGER",
"!j,k.j : dom(a) & k : dom(a) & j < k => a(j) <= a(k)"

theorem "aSize <= maxInt"
theorem "!x.x : dom(a) => (!j.j : x+1..aSize-1 => a(x) < a(j))"
theorem "!x.x : dom(a) => (!j.j : 0..x-1 => a(x) > a(j))"
theorem "!x,k.x : dom(a) & k : myINT & a(x) < k => (!j.j : 0..x => a(j) /= k)"
theorem "!x,k.x : dom(a) & k : myINT & a(x) > k => (!j.j : x..aSize-1 => a(j) /= k)"
theorem "aSize <= MAXINT"
//theorem "!x.x : dom(a) => (!j.j : x+1..aSize-1 => a(j)>a(x))"
//theorem "!x.x : dom(a) => (!j.j : 0..x-1 => a(x) > a(j))"
theorem "!x,k.x : dom(a) & k : INTEGER & a(x) < k => (!j.j : 0..x => j |-> k /: a)"
theorem "!x,k.x : dom(a) & k : INTEGER & a(x) > k => (!j.j : x..aSize-1 => j |-> k /: a)"
theorem "!l,h. l <= h => l <= l + (h - l)/2"
theorem "!l,h. l = h => (h - l)/2 <= h/2 - l/2"
//theorem "!l,h.l : myNAT & h : myNAT & l < h & (h - l) mod 2 = 0 => (h - l)/2 = h/2 - l/2"
//theorem "!l,h.l : myNAT & h : myNAT & l < h & (h - l) mod 2 = 1 & h mod 2 = 0 & l mod 2 = 1 => (h - l)/2 = h/2 - l/2"
//theorem "!l,h.l : myNAT & h : myNAT & l < h & (h - l) mod 2 = 1 & h mod 2 = 1 & l mod 2 = 0 => (h - l)/2 = h/2 - l/2"
//theorem "!l,h.l : myNAT & h : myNAT & l < h => (h - l)/2 <= h/2 - l/2"
theorem "!l,h. l = h => l + (h - l)/2 <= h"
theorem "!l,h. l < h => l + (h - l)/2 <= h"
theorem "!l,h. l <= h => l + (h - l)/2 <= h"
theorem "!l,h. l : dom(a) & h : dom(a) & l <= h => l + (h - l)/2 : dom(a)"
theorem "!l,h. l : 0..aSize & h : -1..aSize-1 & l<=h => l : dom(a) & h : dom(a)"
theorem "!l,h. l : 0..aSize & h : -1..aSize-1 & l<=h => l + (h - l)/2 : dom(a)"
theorem "!x,y. x : myNAT & y : myNAT & x <= y => y - x <= maxInt"

theorem "!x,y,z. x <= y & y <= z => x <= z"
theorem "!x,y. 0 <= x & x <= y & y <= MAXINT => 0 <= y - x & y - x <= MAXINT"
theorem "!x,y. 0 <= x & x <= y & y <= MAXINT => 0 <= (y - x) / 2 & (y - x) / 2 <= MAXINT"
theorem "!x,y. 0 <= x & x <= y & y <= MAXINT => 0 <= x + (y - x) / 2 & x + (y - x) / 2 <= MAXINT"
theorem "!x,y. x : 0..aSize & y : -1..aSize-1 & x <= y => y - x : NATURAL"
theorem "!x,y. x : 0..aSize & y : -1..aSize-1 & x <= y => (y - x) / 2 : NATURAL"
theorem "!x,y. x : 0..aSize & y : -1..aSize-1 & x <= y => x + (y - x) / 2 : NATURAL"


}

procedure(name: "binarySearch", seen: "csts") {
argument "key","myINT"
procedure(name: "binarySearch", seen: "constants_correct") {
argument "key","INTEGER"
result "pos","{-1}\\/dom(a)"

precondition "TRUE=TRUE"
Expand All @@ -54,7 +57,7 @@ mm = new ModelModifier().make {
implementation {
var "low", "low : 0..aSize", "low := 0"
var "high", "high : -1..aSize-1", "high := aSize - 1"
var "mid", "mid : myNAT", "mid := 0"
var "mid", "mid : NATURAL", "mid := 0"

theorem "low > high => 0..low-1 \\/ high+1..aSize-1 = 0..aSize-1"

Expand All @@ -69,8 +72,11 @@ mm = new ModelModifier().make {
}
}
Assert("mid : 0..aSize-1")
While("low <= high", invariant: "mid : 0..aSize-1") {
Assign(" mid := low + (high - low) / 2")
While("low <= high") {
Assert("high - low : NATURAL")
Assert("(high - low) / 2 : NATURAL")
Assert("low + (high - low) / 2 : NATURAL")
Assign("mid := low + (high - low) / 2")
Assert("mid : dom(a)")
If("a(mid) < key") {
Then {
Expand All @@ -96,13 +102,78 @@ mm = new ModelModifier().make {
}
}
}

context(name: "constants_fail", extends: "limits") {
constants "a", "aSize"

axioms "aSize : NATURAL",
"a : 0..aSize-1 --> INTEGER",
"!j.j : dom(a) & j < aSize-1 => a(j) <= a(j+1)",
"aSize = MAXINT",
"MAXINT > 3"

}

procedure(name: "binarySearchFail", seen: "constants_fail") {
argument "key","INTEGER"
result "pos","{-1}\\/dom(a)"

precondition "key /: ran(a)"
postcondition "(pos = -1 => not(key : ran(a))) & (not(pos = -1) => pos : dom(a) & a(pos) = key)"

implementation {
var "low", "low : 0..aSize", "low := 0"
var "high", "high : -1..aSize-1", "high := aSize - 1"
var "mid", "mid : NATURAL", "mid := 0"

theorem "low > high => 0..low-1 \\/ high+1..aSize-1 = 0..aSize-1"

invariants "!x.x : 0..low-1 => x|->key /: a",
"!x.x : high+1..aSize-1 => x|->key /: a"

algorithm {
If("high < low") {
Then {
Assert("high = -1 & a = {}")
Return("high")
}
}
Assert("mid : 0..aSize-1")
While("low <= high", invariant: "mid : 0..aSize-1") {
Assign("mid := low + high")
Assign("mid := mid / 2")
Assert("mid : dom(a)")
If("a(mid) < key") {
Then {
Assign("low := mid + 1")
}
Else {
If("a(mid) > key") {
Then {
Assign("high := mid - 1")
}
Else {
Assert("a[{mid}] = {key}")
Return("mid")
}
}
}
}
}
Assign("high := -1")
Assert("high = -1")
Assert("low > high")
Return("high")
}
}
}
}

m = mm.getModel()
m = new AlgorithmTranslator(m, new AlgorithmGenerationOptions().DEFAULT).run()

mtx = new ModelToXML()
//d = mtx.writeToRodin(m, "GroovyBS", "/tmp")
d = mtx.writeToRodin(m, "GroovyBS", "/tmp")
//d.deleteDir()

"generating a model from an algorithm"

0 comments on commit 27e7fba

Please sign in to comment.