predicate IsEven(n: int)

{

    n % 2 == 0

}

​

predicate IsOdd(n: int)

{

    n % 2 != 0

}

​

predicate IsFirstEven(evenIndex: int, lst: seq<int>)

    requires 0 <= evenIndex < |lst|

    requires IsEven(lst[evenIndex])

{

    forall i :: 0 <= i < evenIndex ==> IsOdd(lst[i])

}

​

predicate IsFirstOdd(oddIndex: int, lst: seq<int>)

    requires 0 <= oddIndex < |lst|

    requires IsOdd(lst[oddIndex])

{

    forall i :: 0 <= i < oddIndex ==> IsEven(lst[i])

}

​

​

method FirstEvenOddIndices(lst : seq<int>) returns (evenIndex: int, oddIndex : int)

    requires |lst| >= 2

    requires exists i :: 0 <= i < |lst| && IsEven(lst[i])

    requires exists i :: 0 <= i < |lst| && IsOdd(lst[i])

    ensures 0 <= evenIndex < |lst|

    ensures 0 <= oddIndex < |lst|

    // This is the postcondition that ensures that it's the first, not just any

    ensures IsEven(lst[evenIndex]) && IsFirstEven(evenIndex, lst)

    ensures IsOdd(lst[oddIndex]) && IsFirstOdd(oddIndex, lst)

{

    for i := 0 to |lst|

        invariant 0 <= i <= |lst|

        invariant forall j :: 0 <= j < i ==> IsOdd(lst[j])

    {

        if IsEven(lst[i])

        {

            evenIndex := i;

            break;

        }

    }

​

    for i := 0 to |lst|

        invariant 0 <= i <= |lst|

        invariant forall j :: 0 <= j < i ==> IsEven(lst[j])

    {

        if IsOdd(lst[i])

        {

            oddIndex := i;

            break;

        }

    }

}

​

method ProductEvenOdd(lst: seq<int>) returns (product : int)

    requires |lst| >= 2

    requires exists i :: 0 <= i < |lst| && IsEven(lst[i])

    requires exists i :: 0 <= i < |lst| && IsOdd(lst[i])

    ensures exists i, j :: 0 <= i < |lst| && IsEven(lst[i]) && IsFirstEven(i, lst) && 

                           0 <= j < |lst| && IsOdd(lst[j])  && IsFirstOdd(j, lst) && product == lst[i] * lst[j]

{

    var evenIndex, oddIndex := FirstEvenOddIndices(lst);

    product := lst[evenIndex] * lst[oddIndex];

}