dafny中的指数方法:可能不会维护不变量
在 Dafny 中，指数方法（exponential method）是一种用于证明程序不变量的技术。它是基于数学归纳法的思想，通过递归地应用程序的规则来证明程序的正确性。
指数方法的基本思路是将程序的每个循环迭代视为一个指数级别的问题规模，然后证明在每个迭代中程序的不变量都得到保持。具体步骤如下：
- 定义循环不变量：首先，需要定义一个循环不变量，它是在每个循环迭代中保持不变的性质或条件。这个不变量通常与程序的语义相关。
- 证明初始化：证明循环不变量在循环的初始状态下成立。
- 证明保持：证明如果循环不变量在某个迭代中成立，那么它在下一个迭代中也成立。
- 证明终止：证明循环终止时，循环不变量仍然成立。
通过以上步骤，可以使用指数方法来证明程序的正确性。在 Dafny 中，可以使用 decreases 关键字来指定循环不变量的指数级别，以确保程序的终止性。
指数方法在证明程序的正确性方面具有一定的优势，它可以帮助开发人员更好地理解程序的行为，并提供了一种形式化的验证手段。它适用于各种类型的程序，特别是涉及循环和递归的程序。
在腾讯云的产品中，与指数方法相关的产品可能是与云计算、人工智能和数据分析相关的服务。以下是一些腾讯云产品的示例：
- 云计算服务：腾讯云服务器（CVM）提供了弹性计算能力，可满足各种规模的计算需求。链接：腾讯云服务器
- 人工智能服务：腾讯云人工智能（AI）平台提供了丰富的人工智能服务，包括图像识别、语音识别、自然语言处理等。链接：腾讯云人工智能
- 数据库服务：腾讯云数据库（TencentDB）提供了可扩展的数据库解决方案，包括关系型数据库、分布式数据库等。链接：腾讯云数据库
请注意，以上仅为示例，具体的产品选择应根据实际需求进行评估和选择。
相关·内容
1回答
下面是用Dafny编写的一个简单的排序算法：
predicate perm(a:array<int>, b:array<int>)
requires a != null && b != null
reads a,b
{
multiset(a[..]) == multiset(b[..])
}
predicate sorted(a:array<int>, min:int, max:int)
requires a != null
requires 0 <= min <= max <= a
浏览 3提问于2017-06-08得票数 2
回答已采纳
我试图理解为什么我下面的断言是失败的。我可以理解这是因为循环不变量，但是为什么Dafny要这样做呢？当我已经清楚地说明了循环条件是while I< n时，为什么它如此依赖于循环不变量？这是因为Dafny先看验证码吗？也就是说，在查看实际代码之前，不变行？ method T ()
{
var n := 10;
var i := 0;
while i < n
invariant 0 <= i <= n + 2
{
i := i + 1;
}
assert i == n;
}
浏览 7提问于2020-09-02得票数 0
我想知道dafny无法验证我的程序是否有原因？ https://rise4fun.com/Dafny/Ip1s 我是不是遗漏了一些额外的不变量？
浏览 19提问于2019-01-19得票数 0
回答已采纳
嗨，为了教学，我准备了一大堆简单的愚蠢的问题。基本上一切都很好，但是...要么我错过了Dafny中关于循环不变量的一些细节，要么这是一个弱点/bug？
method whS(a:int) returns ()
{ var i:int := 0;
while (i<a )
decreases a-i
invariant i<= a
{ assert i<= a;
i:=i+1;
assert i<= a;
}
}
该方法
浏览 47提问于2021-07-31得票数 0
I am used to loops
while Grd
invariant Inv
{ ..}
assert Inv && !Grd;
没有任何中断，Dafny知道Inv && ! Grd是真的，但是: Dafny不检查break;命令后的循环不变量。因此
method tester(s:seq<int>) returns (r:int)
ensures r <= 0
{ var i:nat := |s|;
r := 0;
while (i > 0)
decreases i
invari
浏览 0提问于2020-09-09得票数 2
我想要有一个分配两个迭代器的函数，然后进入一个循环，只要MoveNext()返回true，它就会重复调用迭代器上的MoveNext()。然而，在迭代器上调用MoveNext()会违反(或阻止Dafny验证)另一个迭代器所需的不变量：
iterator Iter1()
{ yield; }
iterator Iter2()
{ yield; }
method main()
decreases *
{
var iter1 := new Iter1();
var iter2 := new Iter2();
var iter1More := true;
va
浏览 13提问于2019-08-07得票数 1
回答已采纳
我在Dafny中有一个带有autocontracts的简单类，它创建了自己的一个新实例。
但是达夫尼说，当我在foo.Add()方法中调用Bar时，“调用可能违反上下文的修改子句”
我不知道为什么会有这个错误，因为这个类没有任何属性
我是不是遗漏了什么？
class {:autocontracts} Foo {
predicate Valid()
constructor() { }
method Add() returns (b:bool)
method Bar() returns (fo:Foo)
ensures fresh(fo)
浏览 9提问于2022-10-18得票数 2
回答已采纳
1回答
我正在研究如何使用dafny来使用“交换”相邻元素来验证插入排序，但是我无法为while循环找到一个合理的不变量，有人能帮我修复它吗？下面是链接：
浏览 10提问于2017-05-19得票数 0
回答已采纳
1回答
我正在研究几种语言的语言比较，这些语言都考虑到了验证(Whiley，Dafny和Frama-C等)。给出了一个函数的示例，该函数将一个数组的区域复制到另一个数组中，在目标数组中具有不同的位置。我想出的规范在Dafny中是这样的：
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
returns (r: array<int>)
// both arrays cannot be null
requires dest != nul
浏览 1提问于2015-12-02得票数 3
回答已采纳
我开始学习Dafny，我只学习了不变量。我有这样的代码：
function pot(m:int, n:nat): int
{
if n==0 then 1
else if n==1 then m
else if m==0 then 0
else pot(m,n-1) * m
}
method Pot(m:int, n:nat) returns (x:int)
ensures x == pot(m,n)
{
x:=1;
var i:=0;
if n==0 {x:=1;}
while i<=n
invariant i<=n;
{
x:=
浏览 8提问于2017-08-18得票数 2
回答已采纳
在Dafny，我正在尝试编写递归规范的迭代实现。更具体地说，当predicate containsMe<T (==)>(l:seq<T>, me:T)是序列l的元素时返回true的me。
在最近被定向到之后，我可以看到其他方法可能更好，尽管如此，我还是遇到了一个有趣的问题。
我有一个部分解决方案(如下所示)，循环开始和结束时给出的断言可以验证，但它不是不变量。我是否遗漏了什么，这是一个bug，或者有什么方法可以帮助Dafny建立我不理解的不变量？
predicate method containsMe<T (==)>(l:seq<T>, me:T
浏览 8提问于2020-08-27得票数 1
1回答
我试图在Dafny中实现并编译一个快速指数算法，但我遇到了一些问题。
上下文：
下面提供了所有的代码；快速指数(FastExp)引理本身是迭代的；是一个exp函数，用来确保计算是正确的(这个函数执行传统的指数不会进入数学是如何进行的，或者它是否工作。这不是问题，数学是正确的。
现在，我遇到的主要问题是：
我不知道如何在循环的减少和invariants;The FastExp引理的后条件“可能不成立”；
如果有人能帮我解决这个简单的问题，我会很高兴的。
提前谢谢你。
function isEven(a: int): bool
requires a >= 0;
{
if a
浏览 6提问于2021-04-19得票数 0
回答已采纳
第一个断言说missing数组中的所有值都是0。另一个表示missing中至少有一个值为0。如果第一个断言为真，则第二个断言也必须为真。
如果有人想要完整的代码，可以在下面给出。它本质上是一个在给定数组中查找缺失数字的程序。
method FindMissing(n: int, a: array<int>) returns (m: int)
requires 2 <= n <= 2 * 100000
requires a.Length == n - 1
requires forall j, k :: 0 <= j < k &
浏览 0提问于2020-04-18得票数 0
我正在检查某个键是否只在数组中出现一次(其中b是返回值)，但是下面的不变量说明它不是由循环维护的： invariant b <==> exists j | 0 <= j < i :: a[j] == key && forall k | 0 <= k < i && j != k :: a[k] != key 循环继续，如下所示 var i := 0;
b := false;
var keyCount := 0;
while i < a.Length
invariant 0 <= i <=
浏览 19提问于2019-10-02得票数 2
回答已采纳
在迭代器上调用MoveNext()时，Dafny显示了多个错误：
iterator Iter()
{}
method main()
decreases *
{
var iter := new Iter();
while (true)
decreases *
{
var more := iter.MoveNext();
if (!more) { break; }
}
}
这些错误发生在调用iter.MoveNext()时：
call may violate context's modifies cl
浏览 0提问于2019-08-06得票数 1
回答已采纳
1回答
一个非常简单的乘法代码：
method Product1 (m: nat, n: nat) returns (res:nat)
ensures res == m * n;
{
var m1: nat := 0;
var n1: nat := 0;
res := 0;
while (m1 < m)
{
n1 := 0;
while (n1 < n)
{
res := res + 1;
n1 := n1 + 1
浏览 3提问于2016-09-14得票数 0
在下面的方法中，Dafny报告does条件可能不起作用，尽管我非常肯定它是成立的。
method toArrayConvert(s:seq<int>) returns (a:array<int>)
requires |s| > 0
ensures |s| == a.Length
ensures forall i :: 0 <= i < a.Length ==> s[i] == a[i] // This is the postcondition that might not hold.
{
a := new int
浏览 1提问于2018-05-22得票数 1
回答已采纳
在阅读了Getting Started with Dafny: A Guide之后，我决定创建我的第一个程序:给定一个整数序列，计算其元素的和。然而，我很难让Dafny来验证这个程序。
function G(a: seq<int>): int
decreases |a|
{
if |a| == 0 then 0 else a[0] + G(a[1..])
}
method sum(a: seq<int>) returns (r: int)
ensures r == G(a)
{
r := 0;
var i: int := 0;
while i
浏览 5提问于2017-06-10得票数 1
1回答
Dafny和事件计数
、、、
我一直在研究Dafny中引理的用法，但是我发现它很难理解，很明显下面的例子无法证实，很可能是因为Dafny没有看到归纳或者类似于一个引理来证明计数的某些性质？基本上，我不知道如何或需要定义什么来帮助达夫尼相信计数是归纳的和其他的东西。一些确保和不变的规范是不必要的，但这不是重点。顺便说一句，这在Spec#中更容易。
function count(items: seq<int>, item: int): nat
decreases |items|
{
if |items| == 0 then 0 else
(if items[|items| - 1] == item
浏览 10提问于2016-02-03得票数 1
回答已采纳
1回答
如果我的索引在每次迭代后都不会减少，我如何避免减少错误？为什么我在对象和数组上使用modify子句时，却在它们上使用modify子句？
class ownerIndexs{
var oi : map<int, int>;
constructor(){
new;
}
}
class multiowned{
var m_numOwners : int;
var m_owners : array<int>;
var m_ownerIndex : ownerIndexs;
method reorganizeOwners() returns (
浏览 13提问于2017-12-30得票数 2
回答已采纳
2回答
达夫尼可以选择设置{:induction false}。而且，据我所知，每当我们在Dafny中使用断言时，在它下面发生了什么，它构造了证明义务，然后使用Z3对它们进行计算。
然而，我读到Z3不支持归纳:例如.然而，任何非平凡的属性都需要通过归纳法来证明.Z3目前不支持归纳证明.()
因此，我的问题是:每当我们设置{:induction true}时，如果不使用Z3，在Dafny中如何执行这种归纳？有不同的潜在求解者吗？有什么启发法吗？最后一个建议是在这里()。
然而，我们讨论的是哪种启发式方法呢？
浏览 39提问于2022-09-26得票数 1
回答已采纳
1回答
如何调用引理作为平等为真的推理。考虑下面的例子，在dafny中，我创建了一个引理，说明从0到n的和是n，选择2。Dafny似乎没有问题证明这个引理是正确的。我想用这个引理来表示，bubblesort中的交换数有一个从0到n的上界，它等于n选择2。在这种情况下，当我试图用引理说它是正确的时，我现在有一个错误。为什么会发生这种情况，我怎么能说平等是真实的，给出一个引理？
method BubbleSort(a: array?<int>) returns (n: nat)
modifies a
requires a != null
ensures n <= (a.Le
浏览 1提问于2021-10-03得票数 1
回答已采纳
我的第一个问题是，我是否可以用Z3Py表示以下公式：
Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])
这意味着:数组中是否存在一个位置i::0<i<|arr|，其值a[i]大于数组avg(arr)的平均值加上给定的阈值t。
我知道这种表达式可以在Dafny中查询，而且(因为Dafny在下面使用Z3 )，我想这可以在Z3Py中完成。
我的第二个问题是: Z3中涉及数组的可判定片段的表达能力如何？我阅读了关于数组的全部理论是如何不可判定的()，而只是一个具体的片段，数组属性片段。
是否有任何有
浏览 8提问于2022-09-19得票数 0
回答已采纳
1回答
我的任务是初始化一个8x8矩阵，并确保矩阵中的所有元素都设置为零。我还需要使用while循环和循环不变量来实现。我的实现如下所示：
method initMatrix(a: array2<int>)
modifies a
// require an 8 x 8 matrix
requires a.Length0 == 8 && a.Length1 == 8
// Ensures that all rows in the matrix are zeroes
ensures forall row, col :: 0 <= r
浏览 2提问于2018-03-27得票数 1
我试图在Dafny中证明简单的gcd算法，所以我写了以下内容，但似乎我不能在循环不变量中使用divides方法： method divides(d: int, x: int) returns (result: bool)
requires d > 0
requires x > 0
ensures (result == true ) ==> (exists q : int :: (d * q == x))
ensures (result == false) ==> (forall q : int :: (d * q != x))
{
浏览 35提问于2019-06-25得票数 0
1回答
我正试着进入达芙妮，但我无法理解以下几点：
var a := new int[10];
var i := 0;
while i < 10
decreases 20 - i
{
a[i] := i;
i := i+1;
}
assert a[5] == 5;
到目前为止，非常简单:声明新数组a并用相应的索引位置初始化它的值。因此，assert语句应该是正确的，但是dafny抱怨说“违反断言”。我试过将a5与其他数字进行比较，例如4和6，以及其他接近的数字，但是它没有起作用，我想知道为什么？
与此相关，我想问一下在dafny (使用VSCode)中打印是如何工作的？
谢谢!
浏览 6提问于2020-12-14得票数 0
1回答
我有以下问题:我必须在Dafny中实现一个优先级队列。我有以下界面：
trait PQSpec {
var nrOfElements: int;
var capacity: int;
var contents: array<int>;
var priorities: array<int>;
predicate Valid()
reads this
{
0 <= nrOfElements <= capacity &&
capacity == contents.Length &&
capacity ==
浏览 7提问于2021-11-14得票数 1
int i = 0
boolean answer = false
while (i < a.length) {
if a[i] == 0
answer = true
i = i + 1
其中'a‘是一个整数数组。我正在做一份试卷，它问我这个的循环不变量是什么，我已经确定了代码可以计算出数组中是否包含0。但到目前为止，我只能认为不变量是
i <= a.length
这个问题要求在不变量中包含变量i，a和答案，所以我知道这不可能是对的。我以前没有遇到过涉及布尔值的循环不变量，我很困惑，有谁能帮助解释一下吗？
浏览 0提问于2014-01-17得票数 2
1回答
不断得到“索引超出范围”
、、、
因此，我尝试在Dafny中实现一个简化的荷兰旗帜问题的程序，其中所有索引0 <= n<k都是红色的，所有索引k <= n< arr.Length都是蓝色的，除了它一直说k可能会越界，尽管根据我的编码方式它最多应该是arr.Length。我在这里做错了什么？
method dutch(arr: array?<char>) returns (k: int)
requires arr != null && forall x :: 0 <= x < arr.Length ==> arr[x] == 'r' || ar
浏览 17提问于2021-03-03得票数 1
1回答
在dafny中是否有一种方法可以创建一个特定于单个循环迭代的不变量？下面，我试图创建一个dafny程序，以上限的掉期数量的泡沫排序。这个值存储在变量n中，所以我想用(a.Length * (a.Length - 1))/2来确定n的上限。原因是，如果数组是相反的，那么在内部循环的第一次迭代中必须有n个交换，然后在内部循环的第二次迭代中进行n-1交换，等等，直到数组被排序。这相当于1+2+3+.+n-1+n= n(n-1)/2，这正是我想要展示的。我想知道，在dafny中是否有一种方法可以根据内部循环的迭代，在下面的代码中对i-j或n的值进行上限。有这样的方法吗？
如果没有，是否有另一种方法来上
浏览 6提问于2021-09-28得票数 1
回答已采纳
我编写了下面的程序来验证数组是否“干净”了任何特定的元素。我很难断言这种方法的结果。在试图断言该方法的结果时，我一直会得到一个断言冲突。
method Main (){
var a:= new int[3];
a[0], a[1], a[2] := 1,2,3;
var v := isClean (a, 1);
assert v == false;
}
method isClean (a : array <int>, key : int) returns (clean : bool)
requires a.Length > 0
浏览 12提问于2020-09-09得票数 1
回答已采纳
2回答
构造函数可以返回原语吗？
、、、
我问这个问题是因为我注意到TypeScript允许声明返回原语类型的构造函数，例如：
type Constructor1 = new () => string; // Primitive string
而不是
type Constructor2 = new () => String; // String object
这让我怀疑JavaScript是否真的允许创建一个函数，该函数在使用new语义调用时返回一个原始值，即传递的值。
function isPrimitive(value) {
return value !== Object(value);
}
不用说，我找不到任
浏览 2提问于2021-12-02得票数 6
回答已采纳
1回答
我从阅读文献中了解到，断言语句只有用户才能看到验证者认为某一点的内容。然而，在我自己的经验中，我看到在引理的情况下，断言语句实际上改变了验证者的想法，并允许证明引理。
有人能澄清吗？
谢谢
浏览 1提问于2020-04-06得票数 0
回答已采纳
我使用了:|运算符并将其转换为while，但现在我不知道如何证明循环将始终返回有效的x。我有以下代码： method test(a : array<int>) returns (z : int)
requires exists x. 0 <= x < a.Length && P(a[x]);
ensures P(a[x]);
{
var x :| 0 <= x < a.Length && P(a[x]);
return x;
} 我把它改成了： method test(a : array<int>
浏览 12提问于2020-01-20得票数 0
回答已采纳
Dafny doens似乎不能证明没有后置条件的两种方法的等价性。这是意料之中的吗？ https://rise4fun.com/Dafny/c88u function method pipeline_func(x: int): int{
x * 2
}
function method program_func(x: int): int {
x + x
}
method pipeline_with_ensures (x: int) returns (x': int)
ensures x' == x*2
{
x' := x*2;
}
浏览 8提问于2019-04-13得票数 1
1回答
我试着用Dafny来验证一个算法。我正在努力修复错误消息“减少表达式可能不会减少(超时)”。我的算法的基本结构如下：
while (U != {})
decreases |S| - |B - U|; // S is a constant and |B| <= |S|
invariant U < B; // U is a subset of B
{
var u :| u in U; // pick an element of u
U := U - {u}; // remove the element
while (...)
浏览 2提问于2020-03-15得票数 0
回答已采纳
我试着使用dafny来验证我的qsort函数的正确性，但是我想知道为什么我的代码已经被验证失败了。这是我的代码：
method Testing (a: array<int>)
requires a.Length > 0
modifies a
{
qsort(a,0,a.Length-1);
var i :int := 0;
while(i<a.Length-1)
decreases a.Length - 1 - i
{
ass
浏览 4提问于2018-04-11得票数 2
回答已采纳
我想询问一个特定的Dafny程序是否验证。Dafny通常用于在visual中以交互方式开发程序。
但是，我需要以一种非交互的方式执行查询。特别是，我需要从python程序中查询Dafny。这个是可能的吗？
浏览 2提问于2016-04-06得票数 0
回答已采纳
这里有几件事我不明白：
0 <= i < a.Length && !(low <= i < high) ==> a[i] != key
在这一行中，为什么我们有！(低<= i<高)？这到底是什么意思？为什么变量我会超出低和高的范围？
，，为什么我们设置low := mid + 1;？我理解这是因为循环可能不会终止(根据dafny告诉我的情况)，但是有人能给我举个例子吗？它发生在哪里，是如何发生的？
predicate sorted(a: array<int>)
reads a
{
forall j, k ::
浏览 1提问于2020-09-07得票数 0
请检查一下下面的代码。其想法只是在每个数组位置添加一个常量(例如+1)。但是dafny返回BP5005: This loop invariant might not be maintained by the loop.作为forall条件。这对我来说没有多大意义，因为循环体确实完成了我们在不变量中定义的内容。
重要的是断言在主方法中是有效的。
method doNothing(arr: array<int>)
modifies arr;
ensures arr.Length == old(arr.Length);
ensures forall i :: 0 <= i <
浏览 1提问于2020-11-25得票数 0
回答已采纳
Rust语言不允许不安全的代码从原始指针后面移出非复制类型，报告下列程序的编译错误：
use std::cell::UnsafeCell;
struct NonCopyType(u32);
fn main() {
let unsafe_cell = UnsafeCell::new(NonCopyType(123));
let ptr = unsafe_cell.get();
// Disallowed, but the code will never access
// the uninitialized unsafe cell after th
浏览 10提问于2022-01-12得票数 2
1回答
给定带有前指针和后指针的队列类型的单链接列表实现，当您从一组1元素中排出一个项时，是否需要将后指针设置为null？
我正在阅读Nell的C++ Plus数据结构，在第5.2章中，他在他的Dequeue方法中写道：
if (front == NULL)
rear == NULL;
我想知道为什么这是必要的。我能想到的唯一原因是他对空集实现Enqueue的方式：
if (rear == NULL)
front = newNode;
else
rear->next = newNode;
rear = newNode;
但是这个条件不能改为if (front == NULL)吗？
浏览 4提问于2016-06-08得票数 1
回答已采纳
我正在考虑将Rust作为我的主要开发语言，而不是Go，所以我一直在阅读文档。
我的工作需要做的一件事就是从多个线程中读取和写入一个自定义数据库，该数据库以单个大型数组的形式存储在内存中，大小可以是32 be。数据库函数旨在避免竞争条件，并在必要时使用互斥锁或原子原语。
Rust文档意味着一个数组只能在单个线程上可变(可写)，或者在多个线程上不可变(只读)，并且不能同时在一个线程上写入和在另一个线程上读取。那么如何使用内存中的数据库呢？这没有意义!
我是不是搞错了？
原谅我，我不能给出任何具体的Rust例子，因为我仍然在学习Rust语法，老实说，在用我所有的时间学习一种我将无法使用的语言之前，我
浏览 0提问于2021-03-13得票数 1
我正在尝试创建一个Dafny程序，当且仅当A不包含重复项时才返回true。 这就是我到目前为止所拥有的，但是不变量invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]);说它不会在entry上保持。 对我做错了什么有什么建议吗？ `method CheckArr1(A: array<int>) returns (r: bool)
requires A.Length > 0
ensures r <==> (forall i, j :: 0
浏览 27提问于2020-04-22得票数 0
回答已采纳
1回答
目前，我正在crm应用程序中开发基于消息imap的模块，并试图使用DDD主体连接点。
我从三个主要实体开始，所有这些实体都受到帐户合计的约束：
帐户-电子邮件帐户。有多个文件夹。
文件夹-文件夹在电子邮件帐户(例如。收件箱，发送，草稿)。有多条消息。
邮件-电子邮件。
在本例中，不变量位于实际集合上，主要在帐户和文件夹之间：
帐户不能有两个同名文件夹，
帐户不能有多个特殊文件夹(如收件箱或发送)，
邮箱应该有实际的邮件计数。
这个设计完美无缺。它保持不变，但几乎每个帐户都有六个左右的文件夹，可以包含数千条消息。加载到内存中的数据量，几乎
浏览 5提问于2021-11-29得票数 0
因此，我在dafny中有一个方法，它接受一个数组a，并返回排序后的版本b。在我的代码中，b := a，然后在b上进行就地插入排序。然而，每当我修改b时，我得到的错误是“赋值可能会更新不在封闭上下文的modifies子句中的数组元素”。我假设这是因为我还没有告诉dafny我将就地修改b。我该如何解决这个问题？
浏览 2提问于2020-11-11得票数 0
1回答
Avl树与红黑树的比较
、、、、
我明天要考试，我的笔记上有3道题我听不懂。
1- #搜索>> #插入和#deletions=0，这是哪一棵树？(Avl或红黑树)(答案是Avl)
2- #insertions>0和#searches=#deletions=0，那是哪棵树？(Avl或红黑树)(答案是红黑)
3- #insertions=#deletions和#searches=0，那是哪棵树？(Avl或红黑树)(答案是红黑)
你能解释一下吗？谢谢你的帮助
浏览 3提问于2015-01-08得票数 1
回答已采纳
1回答
JML，不变量的精确定义
、、、
有人能在Java建模语言中给出以下不变量的准确含义，指出它们之间的主要区别吗？
公共不变量
抽象函数(私有不变量)
表示不变量(私有不变量)
浏览 5提问于2017-07-19得票数 0
指出：
在原子内部使用unsafePerformIO也是危险的，但原因不同。有关此问题的更多信息，请参见unsafeIOToSTM。
当涉及到使用线程和异步异常时，有一些函数可以屏蔽异步异常，以便安全地分配和释放资源。
但是有很多在幕后使用unsafePerformIO的函数，例如memory包中的，强制在STM事务中包含这样一个表达式并不难。这些函数在STM事务中使用实际安全吗？是否存在可能导致内存泄漏或数据损坏的情况？在这种情况下，是否有相当于mask的？
谢谢
浏览 7提问于2020-06-08得票数 7
回答已采纳
我在为我的达菲考试学习，我不知道我的代码有什么问题。
我认为这与我的“超出范围的索引”错误有关，但我不知道如何解决这个问题。
任何提示都将不胜感激。
问题是：
Given an array of characters, it filters all the vowels.
我的方法：
method filterTheVowels(a: array<char>) returns (vowels: array<char>)
requires a.Length > 0
ensures forall i, j | 0 <= i < a.Length &
浏览 8提问于2021-12-05得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
