问题描述
在 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
长的子序列。但我不知道如何有效地表达。
谢谢!
解决方法
我编写了代码,用于从给定的整数数组中查找(最左边)最长的零子序列。由于您可以使用谓词映射 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
}
由于我是 dafny 的新手,任何对风格或任何东西的评论都受到赞赏。