ACL2

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(形式化验证)
(指南)
第35行: 第35行:
 
  $ sudo apt install acl2
 
  $ sudo apt install acl2
 
  $ acl2
 
  $ acl2
 +
ACL2>(@ acl2-version)
 +
"ACL2 Version 8.4"
 
  ACL2 !>:doc max
 
  ACL2 !>:doc max
  

2021年12月24日 (五) 09:58的版本

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

ACL2

目录

简介

ACL2 Theorem Prover

ACL2(A Computational Logic for Applicative Common Lisp,应用 Common Lisp 计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件。

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

编程语言

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

形式化验证

功能

指南

Debian

$ sudo apt install acl2
$ acl2
ACL2>(@ acl2-version)
"ACL2 Version 8.4"
ACL2 !>:doc max

项目

图集

链接

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

变换
操作
导航
工具箱