1 files changed, 0 insertions, 67 deletions
diff --git a/Chalice/tests/refinements/experiments/StringBuilder.chalice b/Chalice/tests/refinements/experiments/StringBuilder.chalice
deleted file mode 100644
index d73f8373..00000000
--- a/Chalice/tests/refinements/experiments/StringBuilder.chalice
+++ /dev/null
@@ -1,67 +0,0 @@
-class Char {}
-class StringBuilder0 {
-  var rep: seq<Char>;
-  method Init()
-    requires acc(rep);
-    ensures acc(rep);
-  { rep := nil<Char>; }  
-  function ToString(): seq<Char>
-    requires rd(rep);
-  { rep }  
-  method Append(chars: seq<Char>)
-    requires acc(rep);
-    ensures acc(rep);
-    ensures ToString() == old(ToString()) ++ chars;
-  { rep := rep ++ chars; }
-}
-
-class Chunk0 {
-  var rep: seq<Char>;  
-  ghost var start;
-}
-
-
-class StringBuilder1 refines StringBuilder0 {
-  var chunks: seq<Chunk0>;
-
-  replaces rep by acc(chunks) && acc(chunks[*].rep) && acc(chunks[*].start) &&
-    /** representation invariant */ null !in chunks && |chunks| > 0 && 
-    chunks[0].start == 0 && 
-    (forall i in [0..|chunks|-1] :: chunks[i+1].start == chunks[i].start + |chunks[i].rep|) && 
-    /** coupling invariant */ (forall c in chunks :: c.rep == rep[c.start..c.start + |c.rep|])
-  
-  refines Init()     
-  {
-    var c := new Chunk0;
-    c.rep := nil<Char>;
-    c.start := 0;
-    chunks := [c];    
-    rep := nil<Char>;   
-  }
-  
-
-  refines Append(chars: seq<Char>)
-  {
-    rep := rep ++ chars;
-    var i; assume 0 <= i && i < |chars|;
-    if (i > 0) {
-      call AppendChunk(chunks[|chunks|-1], chars[..i]);
-    }  
-    if (i < |chars| - 1) {
-      call ExpandByABlock();
-      call AppendChunk(chunks[|chunks|-1], chars[i..]);
-    }
-  }
-
-  method AppendChunk(ch: Chunk0, chars: seq<Char>)
-  {
-    ch.rep := ch.rep ++ chars;
-  }
-  
-  method ExpandByABlock()
-  {
-    var c := new Chunk0;
-    c.rep := nil<Char>;
-    chunks := chunks ++ [c];
-  } 
-}
-\ No newline at end of file