From 60208673a25423e378cc7e9672d5acf9fd6f58bc Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Mon, 7 Jul 2014 15:09:33 -0700
Subject: New logical encoding of types with Is and IsAlloc

---
 Test/dafny1/Celebrity.dfy     | 10 +++++-----
 Test/dafny1/MoreInduction.dfy |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 7e5ab205..360c5aba 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -3,16 +3,16 @@
 
 // Celebrity example, inspired by the Rodin tutorial
 
-static function method Knows<Person>(a: Person, b: Person): bool
+static function method Knows<X>(a: X, b: X): bool
   requires a != b;  // forbid asking about the reflexive case
 
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
+static function IsCelebrity<Y>(c: Y, people: set<Y>): bool
 {
   c in people &&
   (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
 }
 
-method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity0<Z>(people: set<Z>, ghost c: Z) returns (r: Z)
   requires exists c :: IsCelebrity(c, people);
   ensures r == c;
 {
@@ -20,7 +20,7 @@ method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r:
   r := cc;
 }
 
-method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity1<W>(people: set<W>, ghost c: W) returns (r: W)
   requires IsCelebrity(c, people);
   ensures r == c;
 {
@@ -43,7 +43,7 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r:
   r := x;
 }
 
-method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity2<V>(people: set<V>, ghost c: V) returns (r: V)
   requires IsCelebrity(c, people);
   ensures r == c;
 {
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index d71c735f..a52f994b 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -4,7 +4,7 @@
 datatype List<X> = Nil | Cons(Node<X>, List<X>);
 datatype Node<X> = Element(X) | Nary(List<X>);
 
-function FlattenMain<X>(list: List<X>): List<X>
+function FlattenMain<M>(list: List<M>): List<M>
   ensures IsFlat(FlattenMain(list));
 {
   Flatten(list, Nil)
@@ -22,7 +22,7 @@ function Flatten<X>(list: List<X>, ext: List<X>): List<X>
     case Nary(nn) => Flatten(nn, Flatten(rest, ext))
 }
 
-function IsFlat<X>(list: List<X>): bool
+function IsFlat<F>(list: List<F>): bool
 {
   match list
   case Nil => true
-- 
cgit v1.2.3