Paquet : why3 (1.5.1-1 et autres)

Liens pour why3

Ressources Debian :

Télécharger le paquet source why3 :

Responsables :

Ressources externes :

Page d'accueil [why3.lri.fr]

Paquets similaires :

plateforme de vérification logicielle

Why3 est une plateforme pour la vérification déductive de programme. Elle fournit un langage riche pour la spécification et la programmation, appelé WhyML, et repose sur des démonstrateurs externes de théorème, à la fois automatiques et interactifs, pour remplir les conditions de vérification. Why3 est fournie avec une bibliothèque standard de théories logiques (arithmétique des nombres entiers et réels, opérations booléennes, ensembles et leurs relations, etc.) et des structures de données de programmation (tableaux, files d’attente, tables de hachage, etc.). Un utilisateur peut écrire directement des programmes WhyML et obtenir des programmes OCaml correct-par-construction à travers un mécanisme automatique d’extraction. WhyML est aussi utilisé comme langage intermédiaire pour la vérification de de programmes C, Java ou Ada.

Why3 est une réimplémentation complète de l’ancienne plateforme Why. Parmi les nouvelles caractéristiques, il y a de nombreuses extensions pour le langage utilisé, une nouvelle architecture pour appeler des démonstrateurs externes et une API bien conçue permettant d’utiliser Why3 comme bibliothèque logicielle. L’accent est porté sur la modularité et la généricité, permettant à l’utilisateur final de facilement réutiliser des formalisations Why3 ou d’ajouter la prise en charge de nouveaux démonstrateurs.

Étiquettes: Boîte à outils d'interface utilisateur: GTK, Interface utilisateur texte ncurses

Autres paquets associés à why3

dépendances

recommandations

suggestions

enhances

dep: libc6 (>= 2.35)

bibliothèque C GNU : bibliothèques partagées
un paquet virtuel est également fourni par libc6-udeb
dep: libcairo2 (>= 1.2.4)

Bibliothèque graphique vectorielle Cairo 2D
dep: libcairo2-ocaml-zmmv8

paquet virtuel fourni par libcairo2-ocaml
dep: libgdk-pixbuf-2.0-0 (>= 2.22.0)

bibliothèque GDK Pixbuf
dep: libglib2.0-0 (>= 2.35.9)

bibliothèque GLib de routines C
dep: libgtk-3-0 (>= 3.11.5)

bibliothèque d'interface graphique utilisateur GTK
dep: libgtksourceview-3.0-1 (>= 2.91.4)

bibliothèques partagées pour le widget de coloration syntaxique GTK+
dep: liblablgtk3-ocaml-wqgt7

paquet virtuel fourni par liblablgtk3-ocaml
dep: liblablgtksourceview3-ocaml-gh6k6

paquet virtuel fourni par liblablgtksourceview3-ocaml
dep: libpango-1.0-0 (>= 1.14.0)

Mise en place et rendu de texte internationalisé
dep: ocaml-base-4.13.1

paquet virtuel fourni par ocaml-base
dep: tex-common (>= 6.13)

infrastructure commune pour construire et installer TeX
dep: zlib1g (>= 1:1.1.4)

Bibliothèque de compression - binaires

rec: cvc4 (<< 1.9)

automated theorem prover for SMT problems

ou spass

démonstrateur automatique de théorème pour la logique du premier ordre avec égalité

ou z3 (<< 4.11.1)

justificateur de théorème de Microsoft Research

ou alt-ergo (>= 2.0.0)

Paquet indisponible

sug: why3-examples

exemples pour la plateforme de vérification why3

Télécharger why3

Télécharger pour toutes les architectures proposées
Architecture	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
armhf	1.5.1-1+b2	10 172,8 ko	37 120,0 ko	[liste des fichiers]