Dafny

--------------------------------------------------

method sum(n:array<int>), n:int) returns (s:int)
requires a != null && a.Length >= n;
ensures s >= 0;
{
	var i:int i:0;
	while(i<n)
	{
		s:= s +a[i];
		i := i+1;
	}

}


--------------------------------------------------


method memcpy(a:array<int>, b:array<int>, n:int)
modifies b;
requires a!=null && b !=null;
requires n>=0 && a.Length >= n && b.Length >= n;
ensures forall j :: 0 <= j < n ==> a[j] == b[j];
  {
    var i:int := 0;
    
    while( i < n)
	invariant 0 <= i <= n;
	invariant forall j :: 0 <= j < i ==> a[j] == b[j];
    {
      b[i] := a[i];
      
      i := i+1;
    }
  }

  
  
  
  
--------------------------------------------------
  



method max( a:array<int>, n:int ) returns(m:int)
requires a!= null
requires 0 < n <= a.Length;
ensures forall j::(0<=j<n) ==> m >= a[j];
ensures exists j :: (0<=j<n) && m == a[j];
{
  var i:int := 1;
  m := a[0];
  while(i < n)
  invariant 1 <= i <= n;
  invariant forall j::(0<=j<i) ==> m >= a[j];
  {
    if ( a[i] > m) {
      m := a[i];
    }
    
    i := i+1;
  
  }
}


--------------------------------------------------


method find( a:array<int>, n:int, v:int ) returns(pos:int)
requires a!= null
requires 0 < n <= a.Length;
ensures (pos = -1 ==> forall i:: (0<=i<n) => a[i] != v);
ensures (0 <= pos < n) <==> a[pos] == v);
{
  var i:int := 0;
  pos := -1;
  
  while(i < n)
  invariant 0 <= i <= n;
  invariant pos == -1 ==> forall j :: 0 <= j < i ==> a[j] != v;
  invariant 0 <= pos < i <==> a [pos] == v;
  {
    if ( a[i] = v) {
      pos := i;
      break;
    }
    
    i := i+1;
  
  }
}

--------------------------------------------------
method reverse(
....

--------------------------------------------------
method filled(a:array<int>, v:int, n:int) returns (s:bool)
requires a!= null
requires 0 <= n <= a.Length;
ensures s == true ==> forall k :: 0 <= k < n ==> a[k] == v;
ensures s == false ==> exists k :: 0 <= k < n ==> a[k] == v;
{
	var i:int := 0;
	
	while( i < n)
	invariant 0 <= i <= n;
	invariant forall k :: 0 <= k < i ==> a[k] == v;
	{
		if ( a[i] != v) {
			s := false;
			return;
		}
		i := i+1;
	}
	s := true;
}


--------------------------------------------------
method strf(a:array<char>, n: int, b:array<char>, m:int) returns (pos:int)
requires a != null && b != null;
requires 0 <= n < a.Length && 0 <= m < b.Length;
requires n >= m;
ensures pos >= 0 ==> forall k:: 0 <= k < m ==> b[k] ==a[pos+k];
ensures pos == -1 ==> forall k:: 0 <= k < n-m ==> 
						exists p :: 0 <= p < m ==> b[p] !=a [k+p];
{
	pos := -1;
	var i:int := 0;
	while( i < n-m+1 )
	invariant 0<=i<=n;
	{
	
		var j:int := 0;
		while (j<m)
		invariant 0 <= j <= m
		invariant forall k:: 0<=k<j ==> b[k] ==a[i+k];
		{
			if (a[i+j] != b[j]) {
				break;
			}
			j := j+1;
		}
		if( j == m) {
			assert forall k:: 0 <= k < m ==> b[k] == a[i+k];
			return i;
		}
		
		i := i+1;
	}
}




--------------------------------------------------
function fib(n : int) : int // this is the recursive spec of fibonacci
requires n>=0;
{
	if (n==0) then 1 else 
	if (n==1) then 1 else fib(n-1)+fib(n-2)
}

method fibo(n : int) returns (f : int)
requires n >= 0;
ensures f == fib(n);
{
    if (n == 0 || n == 1){
		f := 1;
		return;
	}

	var tmp:int;
    var f:int := 0;
    var next:int := 1;
    
        
	var i:int := 2;
	while( i <= n )
	invariant f == fib(i);
	invariant next == fib(i-1);
    {
        tmp := f + next;
        f := next;		
        next := tmp;
		i := i+1;
    }
    f := next;
}

--------------------------------------------------