标签: hoare-logic

根据许多网站中给出的伪代码，我编写了这个Hoare分区算法，它采用一个数组，根据给定的主元对子数组的开始和结束索引进行分区。它工作得很好，但是有人可以解释一下逻辑，它是如何做到这一点的吗？这是代码：

def hoare(arr,start,end):
     pivot = 4
     i,j = start,end
     while i < j:
        while i < j and arr[i] <= pivot:
            i += 1
        while j >= i and arr[j] > pivot:
            j -= 1
        if i < j:
            arr[i],arr[j] = arr[j],arr[i]
     return j    

分区还有另一种变体，即Lomuto算法。Hoare它做了类似的事情，尽管由于我一开始就不理解该算法，所以我无法发现其中的区别。谁能解释一下算法中发生了什么，以及在哪种情况下哪种算法能提供更好的性能？

我正在教一本关于FOL和程序验证的课程，该课程的灵感来自Morderhai Ben-Ari，《计算机科学的数学逻辑》，施普林格，1993-2012年。我想通过让学生使用Python进行编程来说明这些概念。

对于FOL，我使用的是NLTK，它具有出色的FOL软件包。

但是我还没有找到用于程序验证的Python包：插入前置条件和后置条件逻辑公式，查找循环不变式，逐步验证Python程序等。换句话说，要在Python内使用Hoare逻辑框架并为Python使用程式。

您是否知道此任务的任何包装？

这是算法:

// Precondition: n > 0

l = -1;
r = n;

while (l+1 != r) {
    m = (l+r)/2;

    // I && m == (l+r)/2

    if (a[m] <= x) {
        l = m;
    } else {
        r = m;
    }
}
// Postcondition: -1 <= l < n

我做了一些研究,并将不变量缩小到了if x is in a[0 .. n-1] then a[l] <= x < a[r].

我不知道如何从那里进步.前提似乎过于宽泛,所以我很难显示出来P -> I.

非常感谢任何帮助.这些是可用于证明算法正确性的逻辑规则:

我不确定

{ true } x := y { x = y }

是一个有效的Hoare三重奏.

我不确定是否允许引用变量(在这种情况下y),而不是先在三重程序体中或在前置条件中明确定义它.

{ y=1 } x := y { x = y } //valid

{true} y := 1; x := y { x = y } //valid

如何？

我有我的测试代码(研究WP循环不变量),它在数组单元格中添加两个长整数,每个数字的表示形式:

int main(int argc, const char * argv[]) {

char a[32], b[32];//size can be very big
memset(a, 0, sizeof(a));
memset(b, 0, sizeof(b));
scanf("%s %s", a, b);
unsigned int size1 = strlen(a);
unsigned int size2 = strlen(b);
//code to reverse a string. currently proved 
reverse(a, size1);
reverse(b, size2);
for (unsigned int i = 0; i < size1; i++) a[i]-='0'; //move from chars to integers
for (unsigned int j = 0; j < size2; j++) b[j]-='0';
unsigned int maxsize = size1;
if …