Contract.Requires()和循环不变量的问题
Contract.Requires()是.NET Framework中的一个方法，用于在方法的入口处对输入参数进行前置条件的验证。它用于确保方法在执行之前满足特定的条件，如果条件不满足，则会抛出一个ContractException异常。
循环不变量是在循环执行过程中保持不变的条件或属性。它们是循环正确性的关键部分，用于确保循环的正确执行。循环不变量必须满足以下三个条件：
- 初始化：在循环开始之前，循环不变量必须为真。
- 保持：如果循环不变量在某次迭代之前为真，那么在下一次迭代之前也必须为真。
- 终止：当循环结束时，循环不变量必须为真。
Contract.Requires()和循环不变量在软件开发中起到了不同的作用：
- Contract.Requires()用于在方法的入口处对输入参数进行验证，确保方法在执行之前满足特定的条件，从而提高代码的健壮性和可靠性。
- 循环不变量用于确保循环的正确性，通过定义和验证循环不变量，可以确保循环在每次迭代时都满足特定的条件，从而避免循环陷入无限循环或产生错误的结果。
在云计算领域中，Contract.Requires()和循环不变量的概念并不直接涉及到，它们更多地是与软件开发和代码质量相关的概念。然而，在云计算中，确保代码的正确性和可靠性仍然非常重要，因为云计算涉及到大规模的分布式系统和复杂的网络通信，任何一个错误都可能导致系统的故障或数据的损失。
腾讯云提供了一系列的云计算产品和服务，可以帮助开发者构建可靠和高效的云应用。具体推荐的产品和介绍链接地址可以根据具体的应用场景和需求进行选择。
相关·内容
考虑到这个类，我不知道为什么要得到未被证实的结果!= null警告。
public class MyClass {
private readonly string _value;
public MyClass(string value) {
Contract.Requires(value != null);
_value = value;
}
public string Value {
get {
Contract.Ensures(Contract.Result<string>() != null);
retu
浏览 1提问于2012-06-09得票数 3
回答已采纳
2回答
我想知道如何在.NET Core中正确地使用代码契约，到目前为止，我尝试将CC添加到我的项目、编译和调试中。我对使用Contract.Requires的每个调用中出现的消息和通过googling找到的信息感到困惑。
该信息指出：
程序集必须使用代码契约二进制重写器(CCRewrite)重写，因为它正在调用Contract.Requires<TException>并定义了CONTRACTS_FULL符号。从项目中删除CONTRACTS_FULL符号的任何显式定义并重新构建。CCRewrite ...
正如我所看到的，在项目属性中没有CC选项，正如我所看到的，CC的Github
浏览 1提问于2017-03-09得票数 35
回答已采纳
1回答
是否可以使用方法调用或类似方法禁用类的运行时(和编译时)检查？我在使用带有不变式的类和使用动态构造实例的外部库时遇到了问题。我希望将这些调用包装在我自己的调用中，这些调用接受一个可能部分构造的对象，并返回一个始终有效的对象。
例如，考虑以下代码：
using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
namespace ConsoleApp
{
class Person
{
public string Name { get; set; }
浏览 0提问于2014-11-13得票数 0
日安。
我正在测试C#代码契约。
我一直在研究一些矩阵实现，并希望使用代码契约来进行算术检查(例如。当矩阵乘法有效时)。
为了存储数据，我使用一个一维数组并访问如下所示的数据：
values[r * TotalColumns + c]
r:行到访问
c:要访问的列
我的问题是：
代码契约认为，此访问可能高于数组的上限。
我认为我已经提供了足够的信息，以便系统验证这是不可能的(参见下面的示例)。
我的问题是：
您能看看我的示例代码并向我解释一下，我做错了什么，为什么code Contracts仍然认为这个数组访问是不安全的？
所讨论的代码在GetValue方法中，并标记为注释。
public
浏览 0提问于2016-11-05得票数 1
回答已采纳
1回答
我一直在玩Code Contracts，我真的很喜欢我到目前为止所看到的。它们鼓励我评估并明确声明我的假设，这已经帮助我确定了一些我在添加合同的代码中没有考虑到的角落情况。现在，我正在尝试强制执行更复杂的不变量。我有一个案例目前无法证明，我很好奇除了简单地添加Contract.Assume调用之外，是否还有其他方法可以解决这个问题。以下是正在讨论的类，为了便于阅读，将其简化为：
public abstract class MemoryEncoder
{
private const int CapacityDelta = 16;
private int _currentByte
浏览 0提问于2010-06-19得票数 2
回答已采纳
3回答
我有一个类似于下面这样的类：
class Foo
{
private IEnumerable<Bar> bars;
...
private void DoSomething()
{
Contract.Requires(bars != null);
Contract.Requires(bars.Any());
Bar result = bars.FirstOrDefault(b => SomePredicate) ?? bars.First();
Contract.Assert
浏览 0提问于2011-07-28得票数 3
回答已采纳
我是C#和单元测试的新手，我一直在尝试实现以下构造函数的测试：
public Stepup()
{
InitializeComponent();
}
Stepup是一个分部类，它继承了一个接口。如何为这样的构造函数实现单元测试？除此之外，还有什么方法可以对没有参数的简单构造函数进行单元测试？
浏览 0提问于2013-06-29得票数 1
回答已采纳
假设以下代码：
public class CC3
{
private string _field;
private bool _someFlag;
public string Property
{
get { return _field; }
}
public bool SomeFlag
{
get { return _someFlag; }
}
public void SetField()
{
_field = " foo ";
浏览 3提问于2013-02-19得票数 1
我可以为自动属性指定一个契约，如下所示(取自CC文档中的示例)：
public int MyProperty { get; set ; }
[ContractInvariantMethod]
private void ObjectInvariant () {
Contract. Invariant ( this .MyProperty >= 0 );
...
}
打开运行时检查并尝试将无效值分配给MyProperty时，设置器将抛出System.Diagnostics.Contracts.__ContractsRuntime+ContractException.
有没有办法让它
浏览 1提问于2014-12-22得票数 1
我有以下课程：
public class AndSpecification<TEntity> : ISpecification<TEntity>
{
protected ISpecification<TEntity> First { get; private set; }
protected ISpecification<TEntity> Second { get; private set; }
public bool IsSatisfiedBy(TEntity entity)
{
return
浏览 4提问于2014-10-02得票数 2
回答已采纳
4回答
我有几个关于代码契约的问题，以及使用它们的最佳实践。假设我们有一个类，它有几个属性(例如，参见下面的内容)：
class Class1
{
// Fields
private string _property1; //Required for usage
private List<object> _property2; //Not required for usage
// Properties
public string Property1
{
get
{
r
浏览 3提问于2011-12-05得票数 7
回答已采纳
1回答
这是我的代码：
public class RegularPolygon
{
public int VertexCount;
public double SideLength;
public RegularPolygon(int vertexCount, double sideLength)
{
Contract.Requires(vertexCount >= 3);
VertexCount = vertexCount;
SideLength = sideLength;
}
[Contrac
浏览 25提问于2010-08-12得票数 17
回答已采纳
2回答
我做了一个接口IRequest
public interface IRequest
{
[DataMember(IsRequired = true)]
string EndUserIp { get; set; }
[DataMember(IsRequired = true)]
string TokenId { get; set; }
[DataMember(IsRequired = true)]
string ClientId { get; set; }
[DataMember(IsRequired = true)]
int
浏览 1提问于2014-03-31得票数 4
1回答
代码契约问题
、、、
考虑以下代码：
public class RandomClass
{
private readonly string randomString;
public RandomClass(string randomParameter)
{
Contract.Requires(randomParameter != null);
Contract.Ensures(this.randomString != null);
this.randomString = randomParameter;
}
浏览 0提问于2010-09-16得票数 1
回答已采纳
1回答
我正在尝试将集成到一些现有的代码中，到目前为止，大部分都很好。然而，我面临的问题是，我在一个接口上设置了契约，并且一个实现将实现委托给一个Func<>，该an被传递到类的构造函数中，如下所示：
[ContractClass(typeof(IFooContract))]
public interface IFoo
{
object Bar();
}
[ContractClassFor(typeof(IFoo))]
public abstract class IFooContract : IFoo
{
object IFoo.Bar()
{
C
浏览 1提问于2014-03-07得票数 2
3回答
我不太明白如何确定循环不变量。我知道在循环之前、循环之后和每次循环迭代期间都是正确的，但仅此而已。这是我正在解决的一个示例问题，你如何找到它的循环不变量？
i, temp : integer;
values : array[1..100] of integer;
x := 1;
while x < 100 loop
if values[x] > values[x+1] then begin
temp := values[x];
values[x] := values[x+1];
values[x+1] := temp;
end if;
x
浏览 1提问于2014-04-08得票数 0
此Q3方法通过将n0添加到res |n0| m0来交换m0 *次。如果n0为负，我们将n0和m0都反转为n0*m0 = -n0* -m0成立。
我的问题是，我不知道我的不变量应该是什么样子的，因为不变量需要是布尔型的。有人能告诉我不变布尔条件是什么样子的吗？我想过Abs((n0)-n)*m == res，但那不起作用。
method Q3(n0 : int, m0 : int) returns (res : int)
ensures n0*m0 == res
{
var n, m : int;
res := 0;
if (n0 >= 0)
{n,m := n
浏览 15提问于2017-12-14得票数 2
回答已采纳
我读了一篇关于非线性不变攻击的论文，即非线性不变攻击:对全速尖叫、iSCREAM和Midori64的实际攻击。
我找到了一个sagemath的网站：https://trac.sagemath.org/ticket/21252，在那里，他们有一个代码，可以为任何S盒找到非线性不变量。但这不是官方的，所以不包括在萨格马斯。有人知道怎么做吗？我想用C++编写一个代码来寻找非线性不变量，但我不明白作者的意思。谢谢
浏览 0提问于2021-05-28得票数 2
回答已采纳
3回答
代码契约、空检查和值/引用类型
、、、、
更新的post__：为了避免混淆我正在做和不做的事情，我从根本上编辑了这篇文章，以包含一个导致此问题的完整代码示例。为了使这个帖子可读性无论如何，所有的代码张贴在底部。
背景：
我正在编写一个用于测试的流畅界面(我知道已经完成了，但其中一半的目的是学习它是如何工作的……)，在这个界面中，我想用如下代码行验证myNumber在3到10之间
myNumber.ShouldBeLessThan(10).And.ShouldBeGreaterThan(10);
myListOfCars.ShouldNotBeNull().And.ShouldBeA<IEnumerable<Car>
浏览 0提问于2011-03-08得票数 4
1回答
这是数组问题中一个简单的分离0和1的问题。我搞不懂为什么循环不变量不存在。
method rearrange(arr: array<int>, N: int) returns (front: int)
requires N == arr.Length
requires forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1
modifies arr
ensures 0 <= front <= arr.Length
ensures forall
浏览 3提问于2020-02-19得票数 0
回答已采纳
5回答
当使用形式方面创建一些代码时，是否有通用的方法来确定循环不变量，或者根据问题的不同，它是否会完全不同？
浏览 3提问于2010-05-29得票数 16
回答已采纳
从Cormen等人的“算法概论”。(第三版)，我正在做运动2.1-3。基本上，给定一个长度为A的向量n和一个值v，该算法输出索引i (索引从1开始，而不是0)，如果不存在这样的索引，则输出v = A[i]或NIL。
我的伪码如下：
for j = 1 to length(A):
value = A[j]
if v == value:
return j
return 'NIL'
如何使用循环不变式来证明这是正确的？我不知道如何将他们关于插入排序算法上的循环不变式的讨论扩展到这个算法(称为线性搜索算法)。
我想，当j = 1时，您有一个长度为1的(子
浏览 2提问于2015-11-11得票数 2
回答已采纳
您好，我已经将问题简化为一种简单地将一个数组的元素复制到另一个数组的方法。我的问题是，最终的断言会验证，而初始的断言却无法验证，即使我有一个保护措施来确保初始断言只在第一次进入循环之后应用。因此，我认为最终的断言应该暗示初始的断言。
任何帮助都非常感谢。
method simpImp(a:array<int>) returns (r:array<int>)
{
print "a ",a[..],"\n";
r := new int[a.Length];
var i:nat := 0;
while
浏览 0提问于2020-09-11得票数 1
我是达夫尼的新手，我试图在不使用*的情况下为计算机5*m-3*n编写代码。
有人能告诉我我的密码出了什么问题吗？我认为它是不变的和减少的。
method CalcTerm(m: int, n: nat) returns (res: int)
ensures res == 5*m-3*n;
{
var m1: nat := abs(m);
var n1: nat := n;
res := 0;
while (m1!=0)
invariant m1>=0
decreases m1
{
res := res+5;
m1 := m1-1;
浏览 1提问于2019-07-22得票数 1
回答已采纳
在我的一类中，我有一个ExpandoObject类型的私有字段。这个字段是在constructior (this.expected = new ExpandoObject())中初始化的，所以我确信它永远不会是null。
因此，在这个类中的一个方法中，我安全地添加了
Contract.Assumes(this.expected != null)
在使用this.expected进行任何操作之前，代码契约不必担心对空对象的可能调用。但是，我没有对空引用上可能的方法调用发出警告，而是得到了一个警告：
对方法‘假设’的动态分派调用可能在运行时失败，因为一个或多个适用的重载是条件方法
方法签名和前几
浏览 1提问于2011-03-05得票数 3
嗨，为了教学，我准备了一大堆简单的愚蠢的问题。基本上一切都很好，但是...要么我错过了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
3回答
Hoare逻辑循环不变量
、、、、
我正在研究Hoare Logic，我在理解寻找循环不变量的方法时遇到了问题。
有人能解释一下计算循环不变量的方法吗？
循环不变量应该包含什么才是“有用的”呢？
我只处理简单的例子，寻找不变量，并证明例子中的部分和完全正确，例如：
{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 }
浏览 0提问于2011-01-24得票数 10
回答已采纳
2回答
到目前为止，我一直对循环不变量及其特定性质感到困惑。它们需要在循环之前和之后都是真吗？还是就在循环体本身的某个点？
例如：
int sum = 0;
for (int = 0; i < 10; i++) {
sum += i
}
不变式是，和等于0+ 1 +2+.+ i。在第二次迭代结束时，可以说I= 1，sum =1。这是可行的，但在迭代开始时，不变量也必须是有效的。在循环开始之前和是0，这违反了这个不变式。对吗？
浏览 3提问于2015-02-05得票数 1
回答已采纳
1回答
循环不变vs断言
、、、
这个星期六我有一个编程概念的考试，我很难找到一些信息来更好地理解一些概念。
循环不变和断言有什么区别？对我来说他们看起来一样。
另外，while循环不变性定理究竟是什么？
不确定是我还是很难在网上找到任何关于算法和伪代码的具体信息。
浏览 0提问于2013-01-10得票数 5
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
2回答
考虑一下这种不可变的类型：
public class Settings
{
public string Path { get; private set; }
[ContractInvariantMethod]
private void ObjectInvariants()
{
Contract.Invariant(Path != null);
}
public Settings(string path)
{
Contract.Requires(path != null);
Path =
浏览 1提问于2010-07-29得票数 12
3回答
我试图找到循环的不变量(例如，在下面的代码中)，我真的不知道如何在一般情况下找到不变量。有没有人可以帮我找到一个不变量，也可以帮我找到下面的代码？谢谢
public static int div(int a, int b)
{
int q = 0;
while(a >= b)
{
a -= b;
q++;
}
return q;
}
浏览 0提问于2013-06-09得票数 1
回答已采纳
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
我需要帮助来证明迭代程序的正确性：
def term_ex_2(x,y):
''' Pre: x and y are natural numbers '''
a = x
b = y
while a >= 0 or b >= 0:
if a > 0:
a -= 1
else:
b -= 1
return x * y
我知道我需要以某种方式找到一个循环不变量，并通过对循环进行归纳来证明它。问题是这里的if/else语句把我搞糊涂了。
在此之后，我还必须证明程序是否终止
浏览 11提问于2020-11-12得票数 0
我需要写一个程序来打印两个输入整数的最大公约数，并证明它的正确性。我写了以下内容：
def main():
x = int(input("Enter the first integer: "))
y = int(input("Enter the second integer: "))
print(gcd(x,y))
def gcd(x,y):
if x > y:
smaller = y
else:
smaller = x
for i in range(1, smalle
浏览 0提问于2015-10-24得票数 0
是否可以在某一时间使用反应性扩展调用函数？
例如，如果我想在每天上午9点和下午1点调用foo()方法，我可以使用Timer类每隔几秒钟检查一次，如果是上午9点或下午1点，甚至是Observable.Interval函数。但是否有更有效的方法来做到这一点呢？因此，我并不是每隔几秒钟检查一次是否该调用foo()，而是在正确的时间单独调用foo()。
浏览 5提问于2014-12-13得票数 5
回答已采纳
2回答
我知道循环不变量是用来证明问题的正确性的，但我不太明白如何想出一个循环不变量，不管这个问题有多微不足道。这里有一个例子，有人能指出我应该考虑的步骤是什么吗？我知道循环中所有正在变化的值都必须包含在我的不变量中。请指导我解决这个问题，我也要找到后置条件。一个解释比一个答案更有价值；请帮助。
{M > 0 and N >= 0 }
a = M;
b = N;
k = 1;
while (b > 0) {
if (b % 2 == 0) {
a = a * a;
b = b / 2
} else {
b = b –
浏览 0提问于2015-10-20得票数 4
1回答
//Precondition: n > 0
//Postcondition: returns the minimum number of decial digits
// necessary to write out the number n
int countDigits(int n){
1. int d = 0;
2. int val = n;
3. while(val != 0){
4. val = val / 10; // In C++: 5 / 2 === 2
5. d++;
6. }
浏览 3提问于2014-04-24得票数 0
2回答
证明合并排序输出输入的排列
、、、、
我开始学习计算逻辑，作为练习，我想证明归并排序算法的正确性。
目前，我很难证明这个算法的输出总是与给定输入的排列相对应。
如果有人能帮我解决这个问题，我会很高兴的。
非常感谢
浏览 12提问于2019-10-31得票数 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
我在C# 4.0中使用代码契约。我正在应用通常的静态方法链接来模拟可选参数(我知道C# 4.0支持可选参数，但我真的不想使用它们)。
问题是，如果我调用Init(string , string[])方法，我的合同需求将被执行两次(或者可能是我要实现的链式重载的数量) --这从下面的示例源代码中得到了明显的效果。这可能会很昂贵，特别是由于我使用的File.Exists等相对昂贵的需求。
public static void Init(string configurationPath, string[] mappingAssemblies)
{
// The static contract
浏览 2提问于2010-05-02得票数 4
回答已采纳
1回答
我最近开始读一本关于数据结构的书，它从算法的介绍开始。在一个练习中，它要求通过归纳和循环不变量来证明算法。伪代码中的算法是：
Algorithm DEC2BIN(int n, int[] b)
Input: int n, array b
Output: b[i] contains the i-th bit of n's binary representation.
1: int x=n, k=0;
2:while(x>0){
3: b[k]=x%2;
4: x/=2;
5: k++;
6:}
en of DEC2BIN
我说：
设P(n)是语句"b包含n的二
浏览 2提问于2018-06-17得票数 1
我试图理解为什么我下面的断言是失败的。我可以理解这是因为循环不变量，但是为什么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
我在玩微软的CodeContracts，遇到了一个我无法解决的问题。我有一个包含两个构造器的类：
public Foo (public float f) {
Contracts.Require(f > 0);
}
public Foo (int i)
: this ((float)i)
{}
这个例子被简化了。我不知道如何检查第二个构造函数的f是否大于0。对于合同，这是可能的吗？
浏览 0提问于2009-07-23得票数 1
回答已采纳
2回答
我有以下代码来反转整数中的数字：
public class integerReversal {
public static int reverseNum(int number){
int reversed = 0;
int remainder;
//{I: ; B: number > 0}
while (number > 0){
remainder = number % 10;
number = number / 10;
reversed
浏览 0提问于2015-01-27得票数 0
1回答
我试图从CLRS (算法导论)中解决一些问题，问题7-1有问题。B部分(目前)内容如下：
索引I和j是这样的，以至于我们永远不会访问子数组Ap之外的A元素。r。
我该怎么证明呢？我能看到指数向中间移动但是..。这真是扭曲了我的大脑。解释这不是证据。如果有人能对这个问题有所了解，我会非常感激的。
浏览 8提问于2013-05-29得票数 0
回答已采纳
1回答
我偶然发现了一段我经常使用的代码，它包括在循环中执行算术操作来更新一个数量。重要的一点是，我使用的是中间量，与循环索引无关。我想出了两种写作方法。在这个模拟示例中，我使用标量和向量，但我认为这适用于使用循环更新的几乎每个数量：
scalar coef = someComplicatedScalar;
for (i=0; i<n; i++) {
vector someComplicatedVector;
stuff[i] = someComplicatedScalar * someComplicatedVector;
}
或
scalar coef = someComplica
浏览 1提问于2020-11-21得票数 0
3回答
这两个陈述之间的区别是什么？
Contract.Requires(string.IsNullOrWhiteSpace(userName));
Contract.Assume(string.IsNullOrWhiteSpace(userName));
浏览 0提问于2011-01-21得票数 35
回答已采纳
3回答
对自动实现的属性编写约定代码
、、、、
有没有办法将契约放在.NET中自动实现的属性上？(如果答案是“是”呢？)
(我假设使用来自DevLabs的.NET代码契约)
浏览 0提问于2011-04-01得票数 13
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
实时音视频
即时通信 IM活动推荐
腾讯云开发者
