合约（contract）

在进行Check的时候，会执行contract内的验证内容，验证代码逻辑是否有效

格式说明

contract格式：
node 结点名 ( 输入变量 ) returns ( 输出变量 ) ；
(*@contract
\quad验证结点方法的方法
*)
let
\quad结点方法
tel
验证结点方法的方法：可以定义var、const、assum、guarantee、mode或者import一个外部的contract
mode 格式：
mode 名称 (
\quadrequire 约束条件;
\quadensure 验证结果;
);

不同的mode内的约束条件互不影响
var 格式：
var 变量名
const 格式：
const 常量名
assume 格式
assume 约束条件（可以是一个布尔值true/false，也可也是一个结果为布尔值的公式，如 2 < 3 ）
guarantee 的格式：
guarantee 验证结果（可以是一个布尔值true/false，也可也是一个结果为布尔值的公式，如 a < b ）

对于real类型的变量，在和数值比较大小或赋值的时候，数值一定要带小数，比如a < 0.0，如果写作a < 0则会报错无法执行

范例一

问题描述：验证两个数相乘的代码，如果两个数均为零，则结果一定也为零

代码：


node times (lhs, rhs: real) returns (res: real) ;(*@contractmode absorbing (
require lhs = 0.0 or rhs = 0.0 ;
ensure res = 0.0 ;
) ;*)
let
res = lhs * rhs ;
tel

Check结果：

._one_mode_active为什么Answer结果为falsifiable我暂时不太理解，对目前的验证不是很重要，所以没仔细研究，等我明白了再回来补充

范例二

问题描述：不使用mode，验证两个数相乘的代码，如果两个数均不为零，则结果一定也不为零

代码：

node times (lhs, rhs: real) returns (res: real) ;(*@contractassume lhs <> 0.0 and rhs <> 0.0;guarantee res <> 0.0 ;
*)
let
res = lhs * rhs ;
tel

Check结果：

assume后面写上假设的前提条件

guarantee后面写上，当上述的前提条件满足时，要验证的式子是否有效

a <> b表示a不等于b

范例三

问题描述：验证两个数相乘的代码，如果两个数均为零，则结果一定也为零；如果两个数都大于零或都小于零，则结果一定大于零；如果两个数一个大于零，一个小于零，则结果一定小于零。

代码：

node times (lhs, rhs: real) returns (res: real) ;(*@contract
const zero = 0.0;
mode absorbing (
require lhs = zero or rhs = zero ;
ensure res = zero ;
) ;
mode positive (
require (
rhs > zero and lhs > zero
) or (
rhs < zero and lhs < zero
) ;
ensure res > zero ;
) ;
mode pos_neg (
require (
rhs > zero and lhs < zero
) or (
rhs < zero and lhs > zero ) ; ensure res < zero ; ) ;
*)
let
res = lhs * rhs ;
tel

Check结果：

import一个contract的方法

问题描述：验证两个数相乘的代码，如果两个数均为零，则结果一定也为零

代码：

contract test (lhs, rhs: real) returns (res: real) ;
let
mode absorbing (
require lhs = 0.0 or rhs = 0.0 ;
ensure res = 0.0 ;
) ;
telnode times (lhs, rhs: real) returns (res: real) ;(*@contract
import test (lhs, rhs) returns (res) ;
*)
let
res = lhs * rhs ;
tel

Check结果：

【Kind2（基于SMT的自动模型检查器）学习笔记】contract的用法相关推荐

C++基于ffmpeg和QT开发播放器~学习笔记
C++基于ffmpeg和QT开发播放器 B站网址 https://www.bilibili.com/video/BV1h44y1t7D8?p=2&spm_id_from=pageDriver ...
diy 单片机自动浇花_基于单片机的自动浇花器设计
龙源期刊网 http://www.qikan.com.cn 基于单片机的自动浇花器设计作者:陈赋铭来源:<农家科技下旬刊> 2015 年第 04 期摘要:本文是基于单片机 AT89 ...
c语言打铃器单片机程序,基于单片机的自动打铃器的设计
基于单片机的自动打铃器的设计-电气信息学院毕业设计目录摘要I AbstractII 第一章绪论1 1.1单片机设计的目的和意义1 1.2单片机发展现状和前景展望1 1.2.1课题发展现状1 1 ...
diy 单片机自动浇花_基于单片机的自动浇花器的制作方法
本实用新型涉及浇花设备技术领域,尤其涉及一种基于单片机的自动浇花器. 背景技术: 随着人们生活质量的不断提高,人们喜欢在家里放置花卉来点缀家中环境,从而使花卉种植不断普及,然而大多数花草生长问题是由花 ...
《基于GPU加速的计算机视觉编程》学习笔记
<基于GPU加速的计算机视觉编程>学习笔记(1) 最近打算准备工作 CUDA开发环境(主要是查看N卡的信息) 在WIN10下安装CUDA工具包最近打算在训练模型的时候,感觉电脑非常吃 ...
基于神经网络的机器阅读理解综述学习笔记
基于神经网络的机器阅读理解综述学习笔记一.机器阅读理解的任务定义 1.问题描述机器阅读理解任务可以形式化成一个有监督的学习问题:给出三元组形式的训练数据(C,Q,A),其中,C 表示段落,Q 表示 ...
《基于张量网络的机器学习入门》学习笔记4
<基于张量网络的机器学习入门>学习笔记4 量子概率将概率复数化分布与向量的表示事件与Hilbert空间不兼容属性及其复数概率表示为什么一定要复数概率量子概率将概率复数化在经 ...
图形处理（十三）基于可变形模板的三维人脸重建-学习笔记
基于可变形模板的三维人脸重建-学习笔记原文地址:http://blog.csdn.net/hjimce/article/details/50331423 作者:hjimce 一.数据库处理: 我们通 ...
《深度学习入门-基于Python的理论与实现》学习笔记1
<深度学习入门-基于Python的理论与实现>学习笔记1 第一章Python入门 Python是一个简单.易读.易记的编程语言,可以用类似于英语的语法进行编写程序,可读性高,且能写出高性能 ...
C4D 内置渲染器学习笔记
C4D 内置渲染器学习笔记一.渲染到图片查看器交互式区域渲染这里可以调节渲染画质创建动画预览预览模式:硬件预览图像尺寸可以大一些,这里渲染很快二.渲染设置选择渲染器输出视频保存 ...

【Kind2（基于SMT的自动模型检查器）学习笔记】contract的用法

本章目录

合约（contract）

格式说明

范例一

范例二

范例三

import一个contract的方法

【Kind2（基于SMT的自动模型检查器）学习笔记】contract的用法相关推荐

最新文章

热门文章