Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
inox
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LARA
inox
Commits
e8fa850a
Commit
e8fa850a
authored
14 years ago
by
Swen Jacobs
Browse files
Options
Downloads
Patches
Plain Diff
modified testcases
parent
e0971c9c
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
testcases/InsertionSort.scala
+1
-1
1 addition, 1 deletion
testcases/InsertionSort.scala
testcases/RedBlack.scala
+46
-25
46 additions, 25 deletions
testcases/RedBlack.scala
with
47 additions
and
26 deletions
testcases/InsertionSort.scala
+
1
−
1
View file @
e8fa850a
...
@@ -26,7 +26,7 @@ object InsertionSort {
...
@@ -26,7 +26,7 @@ object InsertionSort {
def
sorted
(
l
:
List
)
:
List
=
(
l
match
{
def
sorted
(
l
:
List
)
:
List
=
(
l
match
{
case
Nil
()
=>
Nil
()
case
Nil
()
=>
Nil
()
case
Cons
(
x
,
xs
)
=>
sortedIns
(
x
,
sorted
(
xs
))
case
Cons
(
x
,
xs
)
=>
sortedIns
(
x
,
sorted
(
xs
))
})
ensuring
(
res
=>
contents
(
res
)
==
contents
(
l
)
&&
isSorted
(
res
))
})
ensuring
(
res
=>
contents
(
res
)
==
contents
(
l
)
)
//
&& isSorted(res))
def
main
(
args
:
Array
[
String
])
:
Unit
=
{
def
main
(
args
:
Array
[
String
])
:
Unit
=
{
val
ls
:
List
=
Cons
(
5
,
Cons
(
2
,
Cons
(
4
,
Cons
(
5
,
Cons
(
1
,
Cons
(
8
,
Nil
()))))))
val
ls
:
List
=
Cons
(
5
,
Cons
(
2
,
Cons
(
4
,
Cons
(
5
,
Cons
(
1
,
Cons
(
8
,
Nil
()))))))
...
...
This diff is collapsed.
Click to expand it.
testcases/RedBlack.scala
+
46
−
25
View file @
e8fa850a
//SJ: I tried to modify this so that funcheck doesn't give Z3 translation
// warnings, but didn't manage quite yet
import
scala.collection.immutable.Set
import
scala.collection.immutable.Set
object
RedBlack
{
object
RedBlack
{
...
@@ -13,10 +16,26 @@ object RedBlack {
...
@@ -13,10 +16,26 @@ object RedBlack {
// Invariant 1. No red node has a red parent
// Invariant 1. No red node has a red parent
def
invariant1
(
t
:
Tree
)
:
Boolean
=
t
match
{
def
invariant1
(
t
:
Tree
)
:
Boolean
=
t
match
{
case
EmptyTree
()
=>
true
case
EmptyTree
()
=>
true
case
Node
(
Black
(),
left
,
_
,
right
)
=>
invariant1
(
left
)
&&
invariant1
(
right
)
case
Node
(
color
,
left
,
_
,
right
)
=>
color
match
{
case
Node
(
Red
(),
Node
(
Red
(),
_
,
_
,
_
),
_
,
_
)
=>
false
case
Black
()
=>
invariant1
(
left
)
&&
invariant1
(
right
)
case
Node
(
Red
(),
_
,
_
,
Node
(
Red
(),
_
,
_
,
_
))
=>
false
case
Red
()
=>
left
match
{
case
Node
(
Red
(),
left
,
_
,
right
)
=>
invariant1
(
left
)
&&
invariant1
(
right
)
case
Node
(
col2
,
_
,
_
,
_
)
=>
col2
match
{
case
Red
()
=>
false
case
_
=>
right
match
{
case
Node
(
col3
,
_
,
_
,
_
)
=>
col3
match
{
case
Red
()
=>
false
case
_
=>
invariant1
(
left
)
&&
invariant1
(
right
)
}
}
}
case
_
=>
right
match
{
case
Node
(
col3
,
_
,
_
,
_
)
=>
col3
match
{
case
Red
()
=>
false
case
_
=>
invariant1
(
left
)
&&
invariant1
(
right
)
}
}
}
}
}
}
/// Invariant 1 END
/// Invariant 1 END
...
@@ -26,24 +45,27 @@ object RedBlack {
...
@@ -26,24 +45,27 @@ object RedBlack {
def
countBlackNodes
(
t
:
Tree
)
:
Int
=
t
match
{
def
countBlackNodes
(
t
:
Tree
)
:
Int
=
t
match
{
case
EmptyTree
()
=>
1
case
EmptyTree
()
=>
1
case
Node
(
Red
(),
left
,
_
,
_
)
=>
countBlackNodes
(
left
)
case
Node
(
color
,
left
,
_
,
_
)
=>
color
match
{
case
Node
(
Black
(),
left
,
_
,
_
)
=>
countBlackNodes
(
left
)
+
1
case
Red
()
=>
countBlackNodes
(
left
)
case
Black
()
=>
countBlackNodes
(
left
)
+
1
}
}
}
def
invariant2
(
t
:
Tree
,
n
:
Int
)
:
Boolean
=
t
match
{
def
invariant2
(
t
:
Tree
,
n
:
Int
)
:
Boolean
=
t
match
{
case
EmptyTree
()
if
n
==
1
=>
true
case
EmptyTree
()
=>
if
(
n
==
1
)
true
else
false
case
EmptyTree
()
=>
false
case
Node
(
color
,
left
,
_
,
right
)
=>
color
match
{
case
Node
(
Red
(),
left
,
_
,
right
)
=>
invariant2
(
left
,
n
)
&&
invariant2
(
right
,
n
)
case
Red
()
=>
invariant2
(
left
,
n
)
&&
invariant2
(
right
,
n
)
case
Node
(
Black
(),
left
,
_
,
right
)
=>
invariant2
(
left
,
n
-
1
)
&&
invariant2
(
right
,
n
-
1
)
case
Black
()
=>
invariant2
(
left
,
n
-
1
)
&&
invariant2
(
right
,
n
-
1
)
}
}
}
/// Invariant 2 END
/// Invariant 2 END
def
member
(
t
:
Tree
,
e
:
Int
)
:
Boolean
=
t
match
{
def
member
(
t
:
Tree
,
e
:
Int
)
:
Boolean
=
t
match
{
case
EmptyTree
()
=>
false
case
EmptyTree
()
=>
false
case
Node
(
_
,
_
,
x
,
_
)
if
x
==
e
=>
true
case
Node
(
_
,
left
,
x
,
right
)
=>
if
(
x
==
e
)
true
case
Node
(
_
,
left
,
x
,
_
)
if
e
<
x
=>
member
(
left
,
e
)
else
if
(
e
<
x
)
member
(
left
,
e
)
case
Node
(
_
,
_
,
_
,
right
)
=>
member
(
right
,
e
)
else
member
(
right
,
e
)
}
}
def
contents
(
t
:
Tree
)
:
Set
[
Int
]
=
t
match
{
def
contents
(
t
:
Tree
)
:
Set
[
Int
]
=
t
match
{
...
@@ -51,33 +73,32 @@ object RedBlack {
...
@@ -51,33 +73,32 @@ object RedBlack {
case
Node
(
_
,
left
,
x
,
right
)
=>
contents
(
left
)
++
contents
(
right
)
++
Set
(
x
)
case
Node
(
_
,
left
,
x
,
right
)
=>
contents
(
left
)
++
contents
(
right
)
++
Set
(
x
)
}
}
def
makeBlack
(
t
:
Tre
e
)
=
{
def
makeBlack
(
t
:
Nod
e
)
=
{
require
(
t
!=
EmptyTree
())
//
require(t != EmptyTree())
//val Node(_, left, x, right) = t
//val Node(_, left, x, right) = t
//Node(Black(), left, x, right)
//Node(Black(), left, x, right)
t
match
{
t
match
{
case
Node
(
_
,
left
,
x
,
right
)
=>
Node
(
Black
(),
left
,
x
,
right
)
case
Node
(
color
,
left
,
x
,
right
)
=>
Node
(
Black
(),
left
,
x
,
right
)
}
}
}
ensuring
((
x
:
Tree
)
=>
x
match
{
case
Node
(
Black
(),
_
,
_
,
_
)
=>
true
;
case
_
=>
false
})
}
ensuring
((
x
:
Tree
)
=>
x
match
{
case
Node
(
Black
(),
_
,
_
,
_
)
=>
true
;
case
_
=>
false
})
def
ins_
(
t
:
Tree
,
e
:
Int
)
:
Tre
e
=
t
match
{
def
ins_
(
t
:
Tree
,
e
:
Int
)
:
Nod
e
=
t
match
{
case
EmptyTree
()
=>
Node
(
Red
(),
EmptyTree
(),
e
,
EmptyTree
())
case
EmptyTree
()
=>
Node
(
Red
(),
EmptyTree
(),
e
,
EmptyTree
())
case
Node
(
color
,
left
,
x
,
right
)
if
x
<
e
=>
balance
(
Node
(
color
,
ins_
(
left
,
e
),
x
,
right
))
case
n
@Node
(
color
,
left
,
x
,
right
)
=>
if
(
x
<
e
)
balance
(
Node
(
color
,
ins_
(
left
,
e
),
x
,
right
))
case
Node
(
color
,
left
,
x
,
right
)
if
x
>
e
=>
balance
(
Node
(
color
,
left
,
x
,
ins_
(
right
,
e
)))
else
if
(
x
>
e
)
balance
(
Node
(
color
,
left
,
x
,
ins_
(
right
,
e
)))
// Element already exists
else
n
//Element already exists
case
t
=>
t
}
}
def
balance
(
t
:
Tre
e
)
:
Tre
e
=
{
def
balance
(
t
:
Nod
e
)
:
Nod
e
=
{
require
(
t
!=
EmptyTree
())
//
require(t != EmptyTree())
t
match
{
t
match
{
case
Node
(
Black
(),
Node
(
Red
(),
Node
(
Red
(),
a
,
x
,
b
),
y
,
c
),
z
,
d
)
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
Node
(
Red
(),
Node
(
Red
(),
a
,
x
,
b
),
y
,
c
),
z
,
d
)
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
Node
(
Red
(),
a
,
x
,
Node
(
Red
(),
b
,
y
,
c
)),
z
,
d
)
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
Node
(
Red
(),
a
,
x
,
Node
(
Red
(),
b
,
y
,
c
)),
z
,
d
)
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
a
,
x
,
Node
(
Red
(),
Node
(
Red
(),
b
,
y
,
c
),
z
,
d
))
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
a
,
x
,
Node
(
Red
(),
Node
(
Red
(),
b
,
y
,
c
),
z
,
d
))
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
a
,
x
,
Node
(
Red
(),
b
,
y
,
Node
(
Red
(),
c
,
z
,
d
)))
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
Node
(
Black
(),
a
,
x
,
Node
(
Red
(),
b
,
y
,
Node
(
Red
(),
c
,
z
,
d
)))
=>
Node
(
Red
(),
Node
(
Black
(),
a
,
x
,
b
),
y
,
Node
(
Black
(),
c
,
z
,
d
))
case
t
=>
t
case
n
@Node
(
_
,
_
,
_
,
_
)
=>
n
}
}
}
ensuring
(
_
=>
true
)
}
//
ensuring (_ => true)
def
insert
(
t
:
Tree
,
e
:
Int
)
:
Tree
=
makeBlack
(
ins_
(
t
,
e
)
)
ensuring
{
res
=>
invariant1
(
res
)
&&
invariant2
(
res
,
countBlackNodes
(
res
))}
def
insert
(
t
:
Tree
,
e
:
Int
)
:
Tree
=
makeBlack
(
ins_
(
t
,
e
)
)
ensuring
{
res
=>
invariant1
(
res
)
&&
invariant2
(
res
,
countBlackNodes
(
res
))}
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment