From 2bd38bc341b4b8a091d4b2f9955b66da72463569 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Wed, 6 Jul 2011 12:12:38 +0000
Subject: [PATCH] abstract memory example from Alloy
---
cp-demo/acl2/AbstractMemory.scala | 31 +++++++++++++++++++++++++++++++
1 file changed, 31 insertions(+)
create mode 100644 cp-demo/acl2/AbstractMemory.scala
diff --git a/cp-demo/acl2/AbstractMemory.scala b/cp-demo/acl2/AbstractMemory.scala
new file mode 100644
index 000000000..923e2a450
--- /dev/null
+++ b/cp-demo/acl2/AbstractMemory.scala
@@ -0,0 +1,31 @@
+import funcheck.Utils._
+import funcheck.Annotations._
+
+import cp.Definitions._
+
+@spec object AbstractMemory {
+ // - our maps are already ``canonicalized''
+
+ def init(): Map[Int,Int] = {
+ Map.empty[Int,Int]
+ }
+
+ def write(memory: Map[Int,Int], address: Int, data: Int): Map[Int,Int] = {
+ memory.updated(address, data)
+ }
+
+ def read(memory: Map[Int,Int], address: Int): Int = {
+ require(memory.isDefinedAt(address))
+ memory(address)
+ }
+
+ def writeRead(m: Map[Int,Int], a: Int, d: Int): Boolean = {
+ (m.updated(a, d))(a) == d
+ } holds
+
+ def writeIdempotent(m: Map[Int,Int], a: Int, d: Int): Boolean = {
+ val m2 = m.updated(a, d)
+ val m3 = m2.updated(a, d)
+ m2 == m3
+ } holds
+}
--
GitLab