文件名称：esverify:使用SMT求解器进行ECMAScript验证
文件大小：135KB
文件格式：ZIP
更新时间：2024-05-22 09:46:00
javascript verification TypeScript
确认 ECMAScript / JavaScript的程序验证（ ）。 Alpha：这仍然是研究原型，尚未投入生产。 文献资料 esverify及其理论基础的详细文档目前正在开发中，将很快发布。 例子 给定一个简单JavaScript max的功能，我们可以使用特殊的伪呼叫添加前置和后置条件requires ，并ensures与布尔表达式。 function max ( a , b ) { requires ( typeof a === "number" ) ; requires ( typeof b === "number" ) ; ensures ( res => res >= a ) ; if ( a >= b ) { return a ; } else { return b ; } } 然后，将使用SMT求解器对这些表达式相对于函数
【文件预览】：
esverify-master
----.gitignore(29B)
----package.json(2KB)
----tslint.json(254B)
----commitlint.config.js(65B)
----package-lock.json(124KB)
----src()
--------parser.ts(37KB)
--------message.ts(5KB)
--------preamble.ts(6KB)
--------scopes.ts(13KB)
--------smt.ts(26KB)
--------qi.ts(12KB)
--------options.ts(778B)
--------javascript.ts(47KB)
--------verification.ts(17KB)
--------logic.ts(40KB)
--------index.ts(2KB)
--------model.ts(23KB)
--------codegen.ts(13KB)
--------util.ts(2KB)
--------vcgen.ts(61KB)
--------interpreter.ts(45KB)
----bin()
--------esverify.js(3KB)
----.travis.yml(453B)
----LICENSE(1KB)
----tsconfig.json(753B)
----tsconfig.module.json(134B)
----examples()
--------fmono.js(1KB)
--------counter.js(325B)
--------strings.js(337B)
--------adder.js(445B)
--------map.js(1KB)
--------reverse-asc.js(2KB)
--------maplen.js(1KB)
--------msort.js(3KB)
--------sumto.js(353B)
--------cons.js(181B)
--------max.js(395B)
--------peano-contradiction.js(2KB)
--------inc.js(153B)
--------f.js(471B)
--------contradiction.js(505B)
--------twice.js(617B)
--------arrays.js(332B)
----README.md(6KB)
----tests()
--------synthesis.ts(7KB)
--------classes.ts(15KB)
--------objects.ts(1KB)
--------higher-order.ts(6KB)
--------arrays.ts(5KB)
--------strings.ts(5KB)
--------mutable-state.ts(4KB)
--------simple.ts(7KB)
--------mergesort.ts(6KB)
--------globals.ts(5KB)
--------helpers.ts(7KB)
--------interpreter.ts(6KB)
--------transform.ts(2KB)
--------api.ts(7KB)
----.editorconfig(147B)