changeset 21:eec6a42fc1c6

Added file for unit test of interval analysis.
author Janus Dam Nielsen <janus.nielsen@alexandra.dk>
date Mon, 25 May 2009 09:43:47 +0200
parents 429e347be685
children 1ef1b5cd92f2
files README examples/while-loop.py pysmcl/test/unit/test.py pysmcl/test/unit/test_intervalanalysis.py
diffstat 4 files changed, 59 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/README	Fri May 22 16:50:47 2009 +0200
+++ b/README	Mon May 25 09:43:47 2009 +0200
@@ -1,21 +1,30 @@
 This project uses the Python module ast, and therefore requires at
 least Python 2.6
 
-A quick overview of the files
+A quick overview of the structure and files
 
-doctests.py: Use this to run all doctests (must be modified when new files get doctests)
-compatibility_check.py: Checks if @secret functions use features outside their scope
-flow.py: Builds a flow graph, and does fixpoint analysis on it
-graph.py: Abstract datatype for a flowgraph, contains a todot method
-util.py: Error-handling
-pretty_print.py: Functions for pretty-printing the python AST-nodes
-secret_annotator.py: Analyses secret variables/expressions
-proof_burden.py: Still only Proof of concept, prints out a proof-burden for openings
-secret_ifs.py: Rewrites secret annotations
-ideal_functionality.py: The decorator is declared here
-test.py: some example code
+pysmcl: Contains the source code of the PySmcl language.
+  compatibility_check.py: Checks if @secret functions use features outside their scope
+  flow.py: Builds a flow graph, and does fixpoint analysis on it
+  graph.py: Abstract datatype for a flowgraph, contains a todot method
+  util.py: Error-handling
+  pretty_print.py: Functions for pretty-printing the python AST-nodes
+  secret_annotator.py: Analyses secret variables/expressions
+  proof_burden.py: Still only Proof of concept, prints out a proof-burden for openings
+  secret_ifs.py: Rewrites secret annotations
+  ideal_functionality.py: The decorator is declared here
+
+pysmcl/test: Various kinds of tests.
+
+pysmcl/tes/unit: Unit tests.
+  doctests.py: Use this to run all doctests (must be modified when new files get doctests)
+     run as python pysmcl/test/unit/doctests.py
+
+Examples: Contains example applications
+  while-loop.py: a basic example
 
 proofexample.thy: experiments with formal proofs in Isabelle
 
-semantics/semantics.tex: A description of the language and analysis
+Semantics: Files related to the description of the language.
+  semantics.tex: A description of the language and analysis.
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/examples/while-loop.py	Mon May 25 09:43:47 2009 +0200
@@ -0,0 +1,32 @@
+
+from pysmcl.ideal_functionality import ideal_functionality
+
+#@proof_burden
+#@ideal_functionality
+def a(c):
+    precondition("c == 5")
+    y = 4
+    a = open(c)
+    if(c>c):
+        pass
+    else:
+        y = 3
+
+
+@ideal_functionality
+def auction(bids):
+    precondition("a >= b <=> bids[a] >= bids[b]")
+    precondition("0 >= bids[0]")
+    precondition("bids[len(bids)-1] >= 0")
+    low = 0
+    high = len(bids)
+    while(low < high):
+        invariant("bids[high] >= 0 && 0 >= bids[low]")
+        mid = (low + high) // 2
+        r = open(bids[mid] >= 0)
+        if r:
+            high = mid
+        else:
+            low = mid
+    result(mid)
+    return mid
--- a/pysmcl/test/unit/test.py	Fri May 22 16:50:47 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-
-from pysmcl.ideal_functionality import ideal_functionality
-
-#@proof_burden
-#@ideal_functionality
-def a(c):
-    precondition("c == 5")
-    y = 4
-    a = open(c)
-    if(c>c):
-        pass
-    else:
-        y = 3
-
-
-@ideal_functionality
-def auction(bids):
-    precondition("a >= b <=> bids[a] >= bids[b]")
-    precondition("0 >= bids[0]")
-    precondition("bids[len(bids)-1] >= 0")
-    low = 0
-    high = len(bids)
-    while(low < high):
-        invariant("bids[high] >= 0 && 0 >= bids[low]")
-        mid = (low + high) // 2
-        r = open(bids[mid] >= 0)
-        if r:
-            high = mid
-        else:
-            low = mid
-    result(mid)
-    return mid
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/test/unit/test_intervalanalysis.py	Mon May 25 09:43:47 2009 +0200
@@ -0,0 +1,5 @@
+
+
+from unittest import TestCase
+
+