ACL2

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(功能)
(项目)
 
第61行: 第61行:
 
*[http://acl2s.ccs.neu.edu ACL2 Sedan theorem prover (ACL2s)] with [[Eclipse]] IDE
 
*[http://acl2s.ccs.neu.edu ACL2 Sedan theorem prover (ACL2s)] with [[Eclipse]] IDE
 
*[https://github.com/biotomas/ipasir ipasir] The [https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=IPASIR____IPASIR Standard Interface] for Incremental Satisfiability Solving(递增可满足性求解)
 
*[https://github.com/biotomas/ipasir ipasir] The [https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=IPASIR____IPASIR Standard Interface] for Incremental Satisfiability Solving(递增可满足性求解)
 +
*[https://github.com/calebegg/proof-pad Proof Pad] is a web based IDE for ACL2, using a [[Kubernetes]] based backend.
  
 
==文档==
 
==文档==

2022年10月13日 (四) 09:25的最后版本

Wikipedia-35x35.png 您可以在Wikipedia上了解到此条目的英文信息 ACL2 Thanks, Wikipedia.

ACL2

Acl2-logo.png

目录

[编辑] 简介

ACL2

ACL2 Theorem Prover

ACL2(A Computational Logic for Applicative Common Lisp,用于通用Lisp的计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2 从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的验证。ACL2 使用 Common Lisp。ACL2 采用 BSD三条款许可证,3-clause BSD 与 GNU GPL 兼容。

ACL2 程序语言可看作是一个函数式(无任何副作用)的 Common Lisp 变体。

[编辑] 功能

[编辑] 指南

A Brief ACL2 Tutorial

Debian

$ sudo apt install acl2
$ acl2
GCL (GNU Common Lisp) ...
ACL2>(@ acl2-version)
"ACL2 Version 8.4"
ACL2 !>:doc max

函数定义

  • defun
  • defunc  ;; with contracts
  • defunec ;; with contracts extending

[编辑] 编程语言

  • ACL2 programming language
  • Yul 编程语言被用作编译以 Solidity 语言编写的Ethereum 智能合约的中间语言。然而,Yul 被设计成比 Solidity 更通用,并可能很快找到更多的应用。
  • Imp 是一种简单的编程语言,主要用于教学目的。
  • Java An ACL2 library for Java

[编辑] 形式化验证

[编辑] 并行计算

Parallel programming in ACL2(p)

[编辑] 项目

ACL2S

[编辑] 文档

ACL2 有自己的一套文档、图书 出版系统,文档的源文件都是 .lisp 结尾, xdoc 包,defxdoc constructors(构造器)函数组成。

XDOC is a tool for documenting ACL2 books.

[编辑] 图书

Books and Papers

  • 《A Computational Logic》
  • 《Computer-Aided Reasoning: An Approach》
  • 《Computer-Aided Reasoning: ACL2 Case Studies》
  • 《Essential Logic for Computer Science》
  • 《Scalable Techniques for Formal Verification》
  • 《Design and Verification of Microprocessor Systems for High-Assurance Applications》
  • 《Formal Verification of Floating-Point Hardware Design: A Mathematical Approach》

[编辑] STEM

[编辑] 图集

[编辑] 链接

分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱