Test/dafny0/Trait/TraitOverride4.dfy


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
28
29
30
31
32
33
34
35
36
37
38
39
40
41

// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"


trait J 
{
	function method F(y: int): int
	
	function method G(y: int): int 
	{ 
	   100 
	}
	
	method M(y: int) returns (kobra:int)
	  requires y > 0;
	  ensures kobra > 0;
	   
	method N(y: int) 
	{ 
	   var x: int;
	   var y : int;
	   y := 10;
	   x := 1000;
	   y := y + x;
	}
}

class C extends J 
{
	function method F(y: int): int 
	{ 
	  200 
	}

	method M(kk:int) returns (ksos:int)
	  requires kk > (-1);
	  ensures ksos > 0;
	{
		ksos:=10;	
	}	 
}