在Dafny中拥有属性的最长序列

method LongestSequenceWithProperty(sequence: array<int>) returns (start: int, length: int)
    ensures start >= 0 && start + length <= sequence.Length;
{
    var maxLength := 0;
    var maxLengthStart := 0;
    var currentLength := 0;
    var currentStart := 0;

    for i: int in 0..sequence.Length-1
        invariant currentStart >= 0 && currentStart < sequence.Length;
        invariant currentLength >= 0 && currentLength <= sequence.Length;
        invariant maxLengthStart >= 0 && maxLengthStart < sequence.Length;
        invariant maxLength >= 0 && maxLength <= sequence.Length;
        invariant maxLength <= currentLength;
        invariant maxLengthStart <= currentStart;
    {
        if sequence[i] satisfies property {
            currentLength := currentLength + 1;
        } else {
            if currentLength > maxLength {
                maxLength := currentLength;
                maxLengthStart := currentStart;
            }
            currentStart := i + 1;
            currentLength := 0;
        }
    }

    if currentLength > maxLength {
        maxLength := currentLength;
        maxLengthStart := currentStart;
    }

    start := maxLengthStart;
    length := maxLength;
}