function rekurrenz(n :int): int
requires n >= 0
ensures rekurrenz(n) > 0
decreases n
{
  if n == 0 then 2 else 3 * rekurrenz(n-1) + 2
} // f(n) = 3 ^ (n+1) - 1 konnte nicht implementiert werden da ^ nicht in Dafny möglich!?

method Rekurrenz(n: int) returns (res:int)
requires n > 0
ensures res == rekurrenz(n)
 {
   var i := 0;
   res := 2;
   while i < n
    invariant 0 <= i <= n
    invariant res == rekurrenz(i)
   {
     res := 3 * res + 2;
     i := i + 1;
   }
 }



 method Main()
 {
   var result:int := Rekurrenz(6);
   print "Rekkurenz(6):= ";
   print result;
   print "\n";

 }