head	1.1;
access;
symbols
	pkgsrc-2026Q1:1.1.0.28
	pkgsrc-2026Q1-base:1.1
	pkgsrc-2025Q4:1.1.0.26
	pkgsrc-2025Q4-base:1.1
	pkgsrc-2025Q3:1.1.0.24
	pkgsrc-2025Q3-base:1.1
	pkgsrc-2025Q2:1.1.0.22
	pkgsrc-2025Q2-base:1.1
	pkgsrc-2025Q1:1.1.0.20
	pkgsrc-2025Q1-base:1.1
	pkgsrc-2024Q4:1.1.0.18
	pkgsrc-2024Q4-base:1.1
	pkgsrc-2024Q3:1.1.0.16
	pkgsrc-2024Q3-base:1.1
	pkgsrc-2024Q2:1.1.0.14
	pkgsrc-2024Q2-base:1.1
	pkgsrc-2024Q1:1.1.0.12
	pkgsrc-2024Q1-base:1.1
	pkgsrc-2023Q4:1.1.0.10
	pkgsrc-2023Q4-base:1.1
	pkgsrc-2023Q3:1.1.0.8
	pkgsrc-2023Q3-base:1.1
	pkgsrc-2023Q2:1.1.0.6
	pkgsrc-2023Q2-base:1.1
	pkgsrc-2023Q1:1.1.0.4
	pkgsrc-2023Q1-base:1.1
	pkgsrc-2022Q4:1.1.0.2
	pkgsrc-2022Q4-base:1.1;
locks; strict;
comment	@# @;


1.1
date	2022.10.08.16.36.47;	author tonio;	state Exp;
branches;
next	;
commitid	vBFQxJRP0pLVZVWD;


desc
@@


1.1
log
@Adding devel/why3 1.5.1

Import from WIP, thanks jihbed.research@@gmail.com

Why3 is a platform for deductive program verification. It provides a rich
language for specification and programming, called WhyML, and relies
on external theorem provers, both automated and interactive, to
discharge verification conditions.
@
text
@Why3 is a platform for deductive program verification. It provides a rich
language for specification and programming, called WhyML, and relies
on external theorem provers, both automated and interactive, to
discharge verification conditions.

Why3 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.). A
user can write WhyML programs directly and get correct-by-construction
OCaml programs through an automated extraction mechanism. WhyML is
also used as an intermediate language for the verification of C, Java,
or Ada programs.
@