小编Cri*_*usa的帖子

的SqlCommand类有一个取消方法是,根据该文件,允许一个取消命令.

我正在寻找通过smo Server类执行的命令的等效方法.该ServerConnection级(服务器类的connectioncontext场)有取消方法,但文档不是它做什么明确的.

我目前正在编写自己的CLR存储过程,我需要使用Microsoft Solver Foundation的解算器.

为了能够在我的CLR项目中添加对Microsft Solver Foundation的引用,我需要将该程序集添加到我的SQL Server实例(源).所以我安装了MS Solver Foundation Redistributable,并使用以下脚本作为服务器管理员在SQL Server中注册它:

USE MYDB

ALTER DATABASE MYDB SET TRUSTWORTHY ON WITH ROLLBACK IMMEDIATE

ALTER DATABASE MYDB SET TRUSTWORTHY ON

CREATE ASSEMBLY MicrosoftSolverFoundation
AUTHORIZATION dbo
FROM 'C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.0\Microsoft.Solver.Foundation.dll' 
WITH PERMISSION_SET = UNSAFE

但是,我收到以下错误:

Assembly 'MicrosoftSolverFoundation' could not be installed because existing policy would keep it from being used.

附加信息

CLR版本:

directory   C:\Windows\Microsoft.NET\Framework64\v4.0.30319\
version v4.0.30319
state   CLR is initialized

SQL Server版本:

Microsoft SQL Server 2012 (SP1) - …

Z3中是否有办法证明/显示给定模型是唯一的，并且不存在其他解决方案？

一个小例子来演示

(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const c1 Int)
(declare-const c2 Int)
(declare-const c3 Int)
(declare-const ra Int)
(declare-const rb Int)
(declare-const rc Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(assert (>= a1 0))
(assert (>= a2 0))
(assert (>= a3 0))
(assert (>= b1 0))
(assert (>= b2 0))
(assert (>= b3 0))
(assert (>= c1 0))
(assert (>= c2 0))
(assert …

我无法证明2个循环不变量:

    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);

我猜测\对于阵列不起作用,正如我所料.

ACSL by Example(第68页,swap_ranges)中有一个类似的函数,它使用了这个函数,但是如上所述,它们无法用WP插件证明这个特定的函数.我在我的机器上试过它,实际上它无法证明相同的不变量.

完整代码

/*
 * memswap()
 *
 * Swaps the contents of two nonoverlapping memory areas.
 * This really could be done faster...
 */

#include "string.h"

/*@
    requires n >= 1;
    requires \valid(((char*)m1)+(0..n-1));
    requires \valid(((char*)m2)+(0..n-1));
    requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
    assigns ((char*)m1)[0..n-1]; …