C# Contract诊断
2024-09-01 11:38:43
命名空间 : using System.Diagnostics.Contracts;
属性标记 : [ContractOption(category: "runtime", setting: "checking", enabled: true)]
事件订阅 : Contract.ContractFailed += (sender, e) => { Console.WriteLine(e.Message); };
1、 Requires() 定义前提条件
static void MinMax(int min,int max)
{
Contract.Requires(min <= max);
Contract.Requires <ArgumentException>(min <= max);
}
static void Preconditions(object o)
{
Contract.Requires<ArgumentNullException>(o != null, "Preconditions, o may not be null");
Console.WriteLine(o.GetType().Name);
}
static void ArrayTest(int [] data)
{
Contract.Requires(Contract.ForAll(data, i => i < ));
Console.WriteLine("ArrayTest contract succeeded");
}
public void ArrayTestWithPureMethod(int [] data)
{
Contract.Requires(Contract.ForAll(data, MyDataCheck));
Console.WriteLine("ArrayWithPureMethod succeeded");
} public int MaxVal { get; set; }
public bool MyDataCheck(int x)
{
return x <= MaxVal;
}
2、 Ensures() 定义后置条件
private static int sharedState = ;
static void Postcondition()
{
Contract.Ensures(sharedState < );
sharedState = ;
Console.WriteLine("change sharedState invariant {0}", sharedState);
sharedState = ;
Console.WriteLine("before returning change it to a valid value {0}", sharedState);
}
static int ReturnValue()
{
Contract.Ensures(Contract.Result<int>() < );
return ;
}
static int ReturnLargerThanInput(int x)
{
Contract.Ensures(Contract.Result<int>() > Contract.OldValue<int>(x));
return x+;
}
static void OutParameters(out int x, out int y)
{
Contract.Ensures(Contract.ValueAtReturn<int>(out x) > && Contract.ValueAtReturn<int>(out x) < );
Contract.Ensures(Contract.ValueAtReturn<int>(out y) % == );
x = ;
y = ;
}
3、 Invariant() 定义在对象的整个生命周期中都必须满足的条件
private int x = ;
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(x > );
} public void Invariant()
{
x = ;
Console.WriteLine("invariant value: {0}", x);
}
4、 Pure特性，可以把方法和类型标记为纯粹的方法，纯粹指的是自定义方法不会修改对象的任何可见状态。
5、 接口协定
[ContractClass(typeof(PersonContract))]
public interface IPerson
{
string FirstName{get;set;}
string LastName { get; set; }
int Age { get; set; }
void ChangeName(string firstName, string lastName);
} [ContractClassFor(typeof(IPerson))]
public abstract class PersonContract:IPerson
{
string IPerson.FirstName
{
get
{
return Contract.Result<string>();
}
set
{
Contract.Requires(value != null);
}
} string IPerson.LastName
{
get
{
return Contract.Result<string>();
}
set
{
Contract.Requires(value != null);
}
} int IPerson.Age
{
get
{
Contract.Ensures(Contract.Result<int>() >= && Contract.Result<int>() < );
return Contract.Result<int>();
}
set
{
Contract.Requires(value >= && value < );
}
} void IPerson.ChangeName(string firstName, string lastName)
{
Contract.Requires(firstName != null);
Contract.Requires(lastName != null);
}
} public class Person:IPerson
{
public Person() { }
public Person(string firstName,string lastName)
{
this.FirstName = firstName;
this.LastName = lastName;
}
public string FirstName
{
get ;
set; } public string LastName
{
get;
set;
} public int Age
{
get;
set;
} public void ChangeName(string firstName, string lastName)
{
this.FirstName = firstName;
this.LastName = lastName;
}
}
最新文章
- MFC双缓冲绘图（2015.09.24）
- 利用mciSendString播放音频
- jira的插件
- bzoj1059: [ZJOI2007]矩阵游戏
- PHP PSR 代码风格
- GCD之barrier
- 5、员工上班时间的问题 - CEO之公司管理经验谈
- 如何解决jQuery easyui中locale文件下easyui-lang-zh_CN中文乱码问题
- adb连接安卓模拟器
- 关于12C中optimizer_adaptive_features参数介绍
- 从rnn到lstm，再到seq2seq（二）
- coursera-斯坦福-机器学习-吴恩达-笔记week3
- python第三方库函数安装
- Azure SQL 数据库仓库Data Warehouse (2) 架构
- oracle 11g 分区表创建（自动按年、月、日分区）
- javascript的事件流
- 趣味编程：CPS风格代码（C++11, C++14版）
- github删除文件夹
- PIE SDK中值滤波
- MapReduce源码分析之作业Job状态机解析（一）简介与正常流程浅析