blob: 016ee117fb738a3d40aaf29db04aec0c0843258b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
constructor C() { }
method Main() // not Main since the enclosing class has a constructor.
{
print "hello, I'm running ... in C\n";
}
}
class D {
method Main() // not Main since it has modifies clause.
modifies this;
{
print "hello, I'm running ... in D\n";
}
}
class E {
static method Main() // not Main since it has requires clause.
requires true;
{
print "hello, I'm running ... in E\n";
}
}
|