简介OpenGL，全称(Open Graphics Library)，是用于渲染2D，3D矢量图形的跨语言、跨平台的应用程序编程接口。这个接口由近350个不同的函数调用组成，用来从简单的图形比特绘制复杂的三维景象。而另一种程序接口系统是仅用于Microsoft Windows上的Direct3D。OpenGL常用于CAD、虚拟实境、科学可视化程序和电子游戏开发。 ------来自百度百科基本...
环境安装Windows 访问 官网 下载并安装，具体安装过程很简单。 使用交互界面，在开始菜单打开Python3 IDLE即可，也可以直接新建一个 filename.py 的文件，写上Python脚本，然后在命令行中输入 python filename.py 运行，还可以用IDLE打开这个文件，按F5运行。MacOS、Linux MacOS和绝大部分Linux发...
带参协议验证带参系统用P(N)表示P = protocolN = 参数的个数参数：具有相同结构的并发执行的主体或者有限个结构不同的主体当N被具体赋值时，就是这个带参系统的一个实例每个主体都能通过规则进行交互规则集R: 刻画带参系统的运行过程相当于每个主体是一个进程，进程之间通过规则进行状态迁移，所有可能发生的事情，都是进程从初始状态通过规则集R中的规则，所到达的状态。带参系统通过调整参数来增...
Murphi简介Murphi工具最初是由Stanford 的 David 教授小组开发的，它是一个枚举模型检查器，具有自己的输入语言，它类似于Unity的保护->动作符号，它们在无限循环中重复执行。Murphi有一个基于显式状态枚举的验证器，这个验证器可以作为状态空间的深度优先或者广度优先搜索来执行，在搜索过程中遇到的状态都保存在Hash表中。Murphi现在仍然在广泛使用，尤其是微处...
AbstractDafny是一种使编写正确代码变得更容易的语言。这里的正确性意味着没有运行错误，并且实际执行了程序员打算执行的操作。为了实现这一目标，Dafny依靠高级注释（annotation）来推理证明代码的正确性。一段代码的效果可以使用高级表达式抽象地描述，这更简单并且更不容易出错。Dafny将编写无错误代码的责任转移到编写无错误注释的代码上例如，Dafny中的以下注释片段表示数组的每...