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

Question

在Dafny中，我试图创建一个Max多态高阶函数，在给定序列和谓词的情况下，该函数返回包含它的最长子序列。例如，最长的递增子序列，或所有元素都为零的最长的子序列。

为此，我设计了一个慢算法(给定P谓词和S序列(：

1. Start an i pivot in the left and a j pivot in the same place.
2. Start the max_sequence = [] and the max_sequence_length = 0.
3. While i<S.length:
counter = 0 
j = i
While max_sequence[i..j] satisfies P and j<S.length:
If counter > max_sequence_length:
max_sequence_length = counter
max_sequence = max_sequence[i..j]
Increment j
Increment i
4. Return max_sequence

你可以看到它的实现：

method maxPropertySequence<T>(P: seq<T> -> bool, sequ: seq<T>) returns (max_seq: seq<T>)
{
var i := 0;
var j := 0;
var longest := 0;
var the_sgmt := sequ;
var fresh_segmnt := sequ;
var counter := longest;
while i<(|sequ|) 
decreases |sequ|-i
{
j := i;
counter := 0;
fresh_segmnt := [sequ[i]];
if P(fresh_segmnt) 
{
j := j+1;
counter:=counter+1;
if counter>longest {
longest:=counter;
the_sgmt := fresh_segmnt;
}
while P(fresh_segmnt) && j<|sequ|
decreases |sequ|-j
{
fresh_segmnt := fresh_segmnt + [sequ[j]];
j := j+1;
counter:=counter+1;
if counter>longest {
longest:=counter;
the_sgmt := fresh_segmnt;
}
}
}
i := i+1;
}
return the_sgmt;

}

我的问题是：如何验证Max函数的行为符合我的预期？更具体地说：我必须添加哪些ensures？

我想了这样的事情：对于原始序列的所有子序列，没有一个子序列包含P并且比the_sgmt长。但我不知道如何有效地表达它。

谢谢！

Answer 1

我编写的代码用于从给定的整数数组中查找(最左边(最长的零子序列。由于可以使用谓词映射sequ，所以这两个问题几乎是相同的。

// For a given integer array, let's find the longest subesquence of 0s.
// sz: size, pos: position.   a[pos..(pos+sz)] will be all zeros
method longestZero(a: array<int>) returns (sz:int, pos:int)   
requires 1 <= a.Length
ensures 0 <= sz <= a.Length
ensures 0 <= pos < a.Length
ensures pos + sz <= a.Length
ensures forall i:int  :: pos <= i < pos + sz ==> a[i] == 0
ensures forall i,j :: (0 <= i < j < a.Length && getSize(i, j) > sz) ==> exists k :: i <= k <= j && a[k] != 0
{
var b := new int[a.Length];   // if b[i] == n, then a[i], a[i-1], ... a[i-n+1] will be all zeros and (i-n ==0 or a[i-n] !=0)
if a[0] == 0
{b[0] := 1;}
else
{b[0] := 0;}
var idx:int := 0;
while idx < a.Length - 1    // idx <- 0 to a.Length - 2
invariant 0 <= idx <= a.Length - 1
invariant forall i:int :: 0 <= i <= idx ==>  0 <= b[i] <= a.Length
invariant forall i:int :: 0 <= i <= idx ==> -1 <= i - b[i]
invariant forall i:int :: 0 <= i <= idx ==> (forall j:int :: i-b[i] < j <= i ==> a[j] == 0) 
invariant forall i:int :: 0 <= i <= idx ==> ( 0 <= i - b[i] ==> a[i - b[i]] != 0 )
{
if a[idx + 1] == 0
{ b[idx + 1] := b[idx] + 1; }
else
{ b[idx + 1] := 0;}
idx := idx + 1;
}

idx := 1;
sz := b[0];
pos := 0;
// Let's find maximum of array b. That is the desired sz.
while idx < a.Length
invariant 1 <= idx <= b.Length
invariant 0 <= sz <= a.Length
invariant 0 <= pos < a.Length
invariant pos + sz <= a.Length
invariant forall i:int :: 0 <= i < idx  ==> b[i] <= sz
invariant forall i:int  :: pos <= i < pos + sz ==> a[i] == 0
invariant forall i, j:int  :: (0 <= i < j < idx && getSize(i,j) > sz) ==>  a[j-b[j]] != 0
{
// find max
if b[idx] > sz 
{ 
sz := b[idx]; 
pos := idx - b[idx] + 1;
}
idx := idx + 1;
}
}

function getSize(i: int, j:int) : int
{
j - i + 1    
}

由于我是新手，任何关于风格或任何东西的评论都会受到赞赏。