框架

排序后的谓词不能访问数组，因为该数组不包含在函数的读取帧中。函数(或谓词)的读取框架是函数允许读取的所有内存位置。限制函数可读内容的原因是，当写入内存时，可以确保没有读取该内存部分的函数具有与之前相同的值。例如，我们可能有两个数组，我们知道其中一个是有序的。如果没有在已排序的谓词上放置reads注释，那么当修改未排序的数组时，就无法确定另一个数组是否停止排序。虽然在这种情况下，我们可以提供不变量来保存它，但在操作数据结构时，它会变得更加复杂。在这种情况下，框架是使核查过程可行的关键。

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
predicate sorted(a: array<int>)
   ...
   reads a
   ...

reads注释不是布尔表达式，就像我们看到的其他注释一样，它可以与前置条件和后置条件一起出现在任何地方。它指定了函数允许访问的一组内存位置，而不是应该为真的属性。数组的名称，就像上面例子中的a，代表该数组的所有元素。也可以指定对象字段和对象集，但我们在这里不讨论这些主题。Dafny将检查您没有读取读取帧中没有声明的任何内存位置。这意味着函数内的函数调用必须具有作为调用函数读取帧子集的读取帧。需要注意的一点是，函数的参数如果不是内存位置，则不需要声明。 框架也会影响方法。正如您可能已经猜到的，它们不需要列出它们所读取的内容，因为我们已经编写了一个方法来访问没有reads注释的数组。方法可以读取它们想要的任何内存，但它们需要用modifies annotation列出它们修改的内存的哪些部分。它们几乎和它们的读取表亲一样，除了它们说的是可以改变什么，而不是函数的值取决于什么。结合读取，修改限制允许Dafny证明代码的属性，否则将非常困难或不可能。读取和修改是允许Dafny一次只处理一个方法的工具之一，因为它们限制了对内存的任意修改，使Dafny能够推理。 请注意，帧化只适用于堆，或通过引用访问的内存。局部变量不是存储在上的，所以它们不能在reads注释中被提及。还请注意，像集合、序列和多集这样的类型都是值类型，它们被视为整数或局部变量。数组和对象是堆引用类型，它们存储在堆上(尽管引用本身和它所指向的值之间总是有微妙的区别)。

练习13

点击查看题目及代码

修改' sorted '谓词的定义，以便当数组被排序且其所有元素都不相同时，它准确地返回true。

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   // Fill in a new body here.
}
predicate sorted(a: array<int>)

练习14

点击查看题目及代码

如果移除前置条件' a != null '会发生什么?更改' sorted '的定义，使其允许参数为null，但如果是则返回false。

predicate sorted(a: array<int>)
   reads a
{
   // Change this definition to treat null arrays as "not sorted".
   // (i.e. return false for null arrays)
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
predicate sorted(a: array<int>)

#