WHY3(1)

💖 WHY3 💖

okay bestie so this is the why3 page from the User Commands section of the manual — yes it's a manual page, yes it's a whole vibe, and yes you're about to understand it. ✨

---

🌸 NAME 🌸

Why3 — it's a software verification platform. that's the whole thing. that's her. 💅

---

🦋 SYNOPSIS 🦋

why3 [general options] <command> [command options] [command arguments]

like… general options first, then a command, then that command's own options and arguments. the order matters, bestie. 🫶

---

✨ DESCRIPTION ✨

So this manual page is just the basic info about the why3 command — a lil summary, a lil appetizer. for the complete tea you gotta go read the Reference Manual. 📖

Why3 is a platform for deductive program verification. it gives you a rich language for specification and programming called whyml, and it relies on external theorem provers — both automated and interactive — to discharge verification conditions. 😤💪

She comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). you can write whyml programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. not me being obsessed with that. 😭💖

and whyml is also used as an intermediate language for the verification of C, Java, or Ada programs. she does it all fr fr.

---

🎀 GENERAL OPTIONS 🎀

• -C <file> — read configuration from <file>. 📂
• --config — same as -C. twin behaviour, no notes.
• --extra-config <file> — read additional configuration from <file>. ✨
• -L <dir> — add <dir> to the library search path. she's looking for her friends 🥺
• --library — same as -L. periodt.
• --debug <flag> — set a debug flag. 🐛
• --debug-all — set all the debug flags that do not change Why3 behaviour. all vibes, zero consequences.
• --list-debug-flags — list known debug flags.
• --list-transforms — list known transformations.
• --list-printers — list known printers.
• --list-provers — list known provers. 👑
• --list-formats — list known input formats.
• --list-metas — list known metas.
• --print-libdir — print location of binary components (plugins, etc). 🧚
• --print-datadir — print location of non-binary data (theories, modules, etc). 🌈
• --version — print version information. the classic.
• -h — print this list of options.
• --help — same as -h. bestie behaviour.

---

💅 COMMANDS 💅

• config — creates a why3 configuration file ~/.why3.conf, containing in particular information about available provers and plugins. if this file already exists, config will only reset unset variables to default value, but will not try to detect provers. 🙈

The subcommand detect forces Why3 to detect again the available provers and to replace them in the configuration file. 🔍

If a supported prover is installed under a name that is not automatically recognized by why3 config, the subcommand add-prover adds a specified binary to the configuration. for example, an Alt-Ergo executable /home/me/bin/alt-ergo-trunk can be added as follows:

why3 config add-prover alt-ergo /home/me/bin/alt-ergo-trunk

slay. 💖

• doc — produces HTML pages from Why3 source code. 🎀
• execute — symbolically executes programs written in the WhyML language. 🏃♀️
• extract — extracts OCaml code from programs written in the WhyML language. 🪄
• ide — launches the graphical user interface of the why3 platform. 👑✨

There are no specific command options. however, at least one command argument must be given. more precisely, the first argument must be the directory of the session. if the directory does not exist, it is created. the other arguments should be existing files that are going to be added to the session. for convenience, if there is only one argument, it can be an existing file, and in this case the session directory is obtained by removing the extension from the file name. iykyk. 💅

• prove — launches why3 in batch mode on a an input file. 🫶
• realize — produces skeleton files for proof assistants. 🦴
• replay — executes the proofs stored in a Why3 session file, as produced by the IDE. 🔁
• session
• wc — produces statistics about Why3 and WhyML source codes. 📊

---

💜 AUTHOR 💜

The information on this manpage was extracted from the complete Why3 reference manual. that's the source, bestie, no cap.

---

🌟 SEE ALSO 🌟

On a debian system, the full documentation for why3 is distributed in PDF and HTML format in the packages why3-doc-html and why3-doc-pdf. it is also available from the why3 homepage <http://why3.lri.fr>. 🌈

---

okay that's the whole page, go verify something, main character. 🔥

Why3 platform — March 2016. mwah, that's the version and date, and that's a wrap. 💖✨🎀🦋