Dafny: berrikuspenen arteko aldeak
Ezabatutako edukia Gehitutako edukia
→Dafny: sarrerako bigarren aparagrafoa orraztuta |
Ezaugarri inperatiboak */ zati bat kode formatuan Etiketa: 2017 wikitestu editorearekin |
||
23. lerroa:
== Ezaugarri inperatiboak ==
<syntaxhighlight lang="Java">
method max(arr:array<int>) returns(max:int)
// Array must have at least one element
requires arr!=null && arr.Length > 0;
// Return cannot be smaller than any element in array
ensures (forall j :int :: (j >= 0 && j < arr.Length ==> max >= arr[j]));
// Return must match some element in array
ensures (exists j : int :: j>=0 && j < arr.Length && max==arr[j]);
{
max:=arr[0];
var i:int :=1;
//
while(i < arr.Length)
// Indent at most arr.Length (needed to show i==arr.Length after loop)
invariant (i<=arr.Length);
// No element seen so far larger than max
invariant (forall j:int :: j>=0 && j<i ==> max >= arr[j]);
// Some element seen so far matches max
invariant (exists j:int :: j>=0 && j<i && max == arr[j]);
// Terminate when i == arr.Length
decreases (arr.Length-i);
{
// Update max if larger element encountered
if(arr[i] > max){max := arr[i];}
// Continue through array
i := i + 1;
}
}
</syntaxhighlight>
== Erreferentziak ==
| |||