Why3
sudo-rsでWhy3が使われていた
sudo-rs/proofs/sudoers.mlw at main · memorysafety/sudo-rs
WhyMLというものが使われている
Why Platform
定理証明支援系っぽい
公式ページ: Why3
ドキュメント: The Why3 Platform — Why3 1.7.2 documentation
Why3のインストール
4. Compilation, Installation — Why3 1.6.0 documentation
opamをインストール
$ opam install why3
code:memo
pogin503@DESKTOP ~
$ opam install why3
The following actions will be performed:
∗ install conf-which 1 required by conf-autoconf
∗ install dune 3.10.0 required by menhir
∗ install ocamlfind 1.9.6 required by why3
∗ install conf-autoconf 0.1 required by why3
∗ install menhirSdk 20230608 required by menhir
∗ install menhirLib 20230608 required by menhir
∗ install num 1.4 required by why3
∗ install menhir 20230608 required by why3
∗ install why3 1.6.0
===== ∗ 9 =====
Do you want to continue? Y/n y
The following system packages will first need to be installed:
autoconf
<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
Let opam run your package manager to install the required system packages?
(answer 'n' for other options) Y/n y
+ /usr/bin/sudo "apt-get" "install" "autoconf"
sudo password for pogin503:
- Reading package lists...
- Building dependency tree...
- Reading state information...
- The following additional packages will be installed:
- automake autotools-dev
- Suggested packages:
- autoconf-archive gnu-standards autoconf-doc libtool gettext
- The following NEW packages will be installed:
- autoconf automake autotools-dev
- 0 upgraded, 3 newly installed, 0 to remove and 118 not upgraded.
- Need to get 940 kB of archives.
- After this operation, 3837 kB of additional disk space will be used.
- Do you want to continue? Y/n
y
- Get:1 http://archive.ubuntu.com/ubuntu jammy/main amd64 autoconf all 2.71-2 338 kB
- Get:2 http://archive.ubuntu.com/ubuntu jammy/main amd64 autotools-dev all 20220109.1 44.9 kB
- Get:3 http://archive.ubuntu.com/ubuntu jammy/main amd64 automake all 1:1.16.5-1.3 558 kB
- Fetched 940 kB in 2s (476 kB/s)
- Selecting previously unselected package autoconf.
(Reading database ... 33891 files and directories currently installed.)
- Preparing to unpack .../autoconf_2.71-2_all.deb ...
- Unpacking autoconf (2.71-2) ...
- Selecting previously unselected package autotools-dev.
- Preparing to unpack .../autotools-dev_20220109.1_all.deb ...
- Unpacking autotools-dev (20220109.1) ...
- Selecting previously unselected package automake.
- Preparing to unpack .../automake_1%3a1.16.5-1.3_all.deb ...
- Unpacking automake (1:1.16.5-1.3) ...
- Setting up autotools-dev (20220109.1) ...
- Setting up autoconf (2.71-2) ...
- Setting up automake (1:1.16.5-1.3) ...
- update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode
- Processing triggers for install-info (6.8-4build1) ...
- Processing triggers for man-db (2.10.2-1) ...
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed conf-which.1
⬇ retrieved menhir.20230608 (https://opam.ocaml.org/cache)
⬇ retrieved dune.3.10.0 (https://opam.ocaml.org/cache)
∗ installed conf-autoconf.0.1
⬇ retrieved menhirSdk.20230608 (cached)
⬇ retrieved num.1.4 (https://opam.ocaml.org/cache)
⬇ retrieved menhirLib.20230608 (https://opam.ocaml.org/cache)
⬇ retrieved ocamlfind.1.9.6 (https://opam.ocaml.org/cache)
⬇ retrieved why3.1.6.0 (https://opam.ocaml.org/cache)
∗ installed ocamlfind.1.9.6
∗ installed num.1.4
∗ installed dune.3.10.0
∗ installed menhirSdk.20230608
∗ installed menhirLib.20230608
∗ installed menhir.20230608
∗ installed why3.1.6.0
Done.
ドキュメント: https://www.why3.org/doc/
#形式手法 #OCaml