summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/Compilation.dfy8
-rw-r--r--Test/dafny0/Modules1.dfy2
-rw-r--r--Test/dafny0/Modules2.dfy2
-rw-r--r--Test/dafny0/OpaqueFunctions.dfy4
-rw-r--r--Test/dafny3/CachedContainer.dfy.expect1
-rw-r--r--Test/dafny3/GenericSort.dfy2
-rw-r--r--Test/dafny4/Bug110.dfy2
-rw-r--r--Test/dafny4/Bug117.dfy4
-rw-r--r--Test/irondafny0/Queue.dfyi2
-rw-r--r--Test/irondafny0/opened_workaround.dfy2
-rw-r--r--Test/irondafny0/xrefine1.dfy6
-rw-r--r--Test/irondafny0/xrefine2.dfy6
-rw-r--r--Test/irondafny0/xrefine3.dfy6
13 files changed, 24 insertions, 23 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 965f0787..7a443e47 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -109,8 +109,8 @@ module T refines S {
}
}
module A {
- import X as S default T
- import Y as S default T
+ import X : T
+ import Y : T
import Z = T
method run() {
var x := new X.C;
@@ -128,7 +128,7 @@ method NotMain() {
abstract module S1 {
- import B as S default T
+ import B : T
method do()
}
@@ -138,7 +138,7 @@ module T1 refines S1 {
}
}
module A1 {
- import X as S1 default T1
+ import X : T1
method run() {
X.do();
var x := new X.B.C;
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 3ffa5a23..3025cc00 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -130,6 +130,6 @@ abstract module Regression {
abstract module B
{
- import X as A
+ import X : A
}
}
diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
index a8dde8ce..beb80546 100644
--- a/Test/dafny0/Modules2.dfy
+++ b/Test/dafny0/Modules2.dfy
@@ -31,7 +31,7 @@ module Test {
}
module Test2 {
- import opened B as A
+ import opened B : A
method m() {
var c := new C; // fine, as A was opened
var c' := new B.C;// also fine, as A is bound
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index e1c0756c..b3cde309 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -44,7 +44,7 @@ module A' refines A {
}
module B {
- import X as A
+ import X : A
method Main() {
var c := new X.C();
c.M(); // fine
@@ -68,7 +68,7 @@ module B {
}
}
module B_direct {
- import X as A'
+ import X : A'
method Main() {
var c := new X.C();
c.M(); // fine
diff --git a/Test/dafny3/CachedContainer.dfy.expect b/Test/dafny3/CachedContainer.dfy.expect
index c6c90498..0185aacd 100644
--- a/Test/dafny3/CachedContainer.dfy.expect
+++ b/Test/dafny3/CachedContainer.dfy.expect
@@ -1,2 +1,3 @@
+CachedContainer.dfy(120,25): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B"
Dafny program verifier finished with 47 verified, 0 errors
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index ea75c196..7555817c 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -17,7 +17,7 @@ abstract module TotalOrder {
}
abstract module Sort {
- import O as TotalOrder // let O denote some module that has the members of TotalOrder
+ import O : TotalOrder // let O denote some module that has the members of TotalOrder
predicate Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length
diff --git a/Test/dafny4/Bug110.dfy b/Test/dafny4/Bug110.dfy
index 239f18d3..aa808669 100644
--- a/Test/dafny4/Bug110.dfy
+++ b/Test/dafny4/Bug110.dfy
@@ -27,5 +27,5 @@ abstract module Host {
}
abstract module Main {
- import H as Host
+ import H : Host
}
diff --git a/Test/dafny4/Bug117.dfy b/Test/dafny4/Bug117.dfy
index 2ae4bc70..418746cb 100644
--- a/Test/dafny4/Bug117.dfy
+++ b/Test/dafny4/Bug117.dfy
@@ -8,14 +8,14 @@ abstract module AbstractModule1
abstract module AbstractModule2
{
- import opened AM1 as AbstractModule1
+ import opened AM1 : AbstractModule1
datatype AbstractType2 = AbstractType2(x:AbstractType1)
}
abstract module AbstractModule3
{
- import AM1 as AbstractModule1
+ import AM1 : AbstractModule1
datatype AbstractType2 = AbstractType2(x:AM1.AbstractType1)
}
diff --git a/Test/irondafny0/Queue.dfyi b/Test/irondafny0/Queue.dfyi
index 9f7eb534..06f4b29e 100644
--- a/Test/irondafny0/Queue.dfyi
+++ b/Test/irondafny0/Queue.dfyi
@@ -17,6 +17,6 @@ abstract module Queue {
}
abstract module MainSpec {
- import Q as Queue
+ import Q : Queue
}
diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
index 7464c346..6d44ccfd 100644
--- a/Test/irondafny0/opened_workaround.dfy
+++ b/Test/irondafny0/opened_workaround.dfy
@@ -17,5 +17,5 @@ abstract module B {
}
abstract module C {
- import Bee as B // Works
+ import Bee : B // Works
}
diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy
index 4b085e6b..1b835649 100644
--- a/Test/irondafny0/xrefine1.dfy
+++ b/Test/irondafny0/xrefine1.dfy
@@ -9,7 +9,7 @@ abstract module ProtocolSpec {
abstract module HostSpec {
type HostT
- import P as ProtocolSpec
+ import P : ProtocolSpec
function method foo(h:HostT) : P.ProtoT
}
@@ -42,8 +42,8 @@ module HostImpl exclusively refines HostSpec {
}
abstract module MainSpec {
- import HI as HostSpec
- import PI as ProtocolSpec
+ import HI : HostSpec
+ import PI : ProtocolSpec
method Test(h1:HI.HostT, h2:HI.HostT)
requires HI.foo(h1) == HI.foo(h2);
diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy
index 1de4e201..9c33391b 100644
--- a/Test/irondafny0/xrefine2.dfy
+++ b/Test/irondafny0/xrefine2.dfy
@@ -9,7 +9,7 @@ abstract module ProtocolSpec {
abstract module HostSpec {
type HostT
- import P as ProtocolSpec
+ import P : ProtocolSpec
function method foo(h:HostT) : P.ProtoT
}
@@ -42,8 +42,8 @@ module HostImpl exclusively refines HostSpec {
}
abstract module MainSpec {
- import HI as HostSpec
- import PI as ProtocolSpec
+ import HI : HostSpec
+ import PI : ProtocolSpec
method Test(h1:HI.HostT, h2:HI.HostT)
requires HI.foo(h1) == HI.foo(h2);
diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy
index 44add7cc..86dbd957 100644
--- a/Test/irondafny0/xrefine3.dfy
+++ b/Test/irondafny0/xrefine3.dfy
@@ -12,7 +12,7 @@ abstract module AlphaSpec {
abstract module BetaSpec {
type Beta
- import A as AlphaSpec
+ import A : AlphaSpec
predicate IsValid(b:Beta)
@@ -49,8 +49,8 @@ module BetaImpl exclusively refines BetaSpec {
}
abstract module MainSpec {
- import A as AlphaSpec
- import B as BetaSpec
+ import A : AlphaSpec
+ import B : BetaSpec
method Main()
{
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 14:55:12 +0000