[ Paquet source : why3 ]
Paquet : why3 (1.8.1-1 et autres)
Liens pour why3
Ressources Debian :
- Rapports de bogues
- Developer Information
- Journal des modifications Debian
- Fichier de licence
- Suivis des correctifs pour Debian
Télécharger le paquet source why3 :
Responsables :
Ressources externes :
- Page d'accueil [www.why3.org]
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.
Autres paquets associés à why3
|
|
|
|
-
- dep: libc6 (>= 2.32) [x32]
- bibliothèque C GNU : bibliothèques partagées
un paquet virtuel est également fourni par libc6-udeb
- dep: libc6 (>= 2.38) [non alpha, ia64, loong64, sh4, x32]
- dep: libc6 (>= 2.41) [loong64, sh4]
-
- dep: libc6.1 (>= 2.37) [ia64]
- bibliothèque C GNU : bibliothèques partagées
un paquet virtuel est également fourni par libc6.1-udeb
- dep: libc6.1 (>= 2.38) [alpha]
-
- dep: libcairo2 (>= 1.12.0) [x32]
- Bibliothèque graphique vectorielle Cairo 2D
- dep: libcairo2 (>= 1.2.4) [amd64, arm64, ppc64el, riscv64, s390x]
-
- dep: libcairo2-ocaml-3tam5 [s390x]
- paquet virtuel fourni par libcairo2-ocaml
-
- dep: libcairo2-ocaml-awcl2 [non alpha, amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par libcairo2-ocaml
-
- dep: libcairo2-ocaml-eesc3 [amd64, arm64, ppc64el, riscv64]
- paquet virtuel fourni par libcairo2-ocaml
-
- dep: libcairo2-ocaml-vad17 [ia64]
- paquet virtuel fourni par libcairo2-ocaml
-
- dep: libcairo2-ocaml-xxkq1 [alpha]
- paquet virtuel fourni par libcairo2-ocaml
-
- dep: libfontconfig1 (>= 2.12.6) [x32]
- Bibliothèque de configuration de polices générique - exécutables
-
- dep: libfreetype6 (>= 2.2.1) [x32]
- moteur de fontes FreeType 2, fichiers de bibliothèques partagées
-
- dep: libgdk-pixbuf-2.0-0 (>= 2.22.0) [amd64, arm64, ppc64el, riscv64, s390x, x32]
- bibliothèque GDK Pixbuf
-
- dep: libglib2.0-0 (>= 2.35.9) [x32]
- bibliothèque GLib de routines C – paquet de transition
-
- dep: libglib2.0-0t64 (>= 2.36.0) [amd64, arm64, ppc64el, riscv64, s390x]
- bibliothèque GLib de routines C
-
- dep: libgmp10 (>= 2:6.3.0+dfsg) [amd64, arm64, ppc64el, riscv64, s390x]
- Bibliothèque arithmétique à multi-précision
-
- dep: libgtk-3-0 (>= 3.9.10) [x32]
- bibliothèque d'interface graphique utilisateur GTK
-
- dep: libgtk-3-0t64 (>= 3.11.5) [amd64, arm64, ppc64el, riscv64, s390x]
- bibliothèque d'interface graphique utilisateur GTK
-
- dep: libgtksourceview-3.0-1 (>= 2.91.4) [amd64, arm64, ppc64el, riscv64, s390x, x32]
- bibliothèques partagées pour le widget de coloration syntaxique GTK+
-
- dep: liblablgtk3-ocaml-285x5 [alpha]
- paquet virtuel fourni par liblablgtk3-ocaml
-
- dep: liblablgtk3-ocaml-4l5z8 [non alpha, amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par liblablgtk3-ocaml
-
- dep: liblablgtk3-ocaml-a7bg7 [amd64, arm64, ppc64el, riscv64]
- paquet virtuel fourni par liblablgtk3-ocaml
-
- dep: liblablgtk3-ocaml-qi0e5 [s390x]
- paquet virtuel fourni par liblablgtk3-ocaml
-
- dep: liblablgtk3-ocaml-zkf21 [ia64]
- paquet virtuel fourni par liblablgtk3-ocaml
-
- dep: liblablgtksourceview3-ocaml-5g7c1 [non alpha, amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par liblablgtksourceview3-ocaml
-
- dep: liblablgtksourceview3-ocaml-b8319 [alpha]
- paquet virtuel fourni par liblablgtksourceview3-ocaml
-
- dep: liblablgtksourceview3-ocaml-udvc2 [ia64]
- paquet virtuel fourni par liblablgtksourceview3-ocaml
-
- dep: liblablgtksourceview3-ocaml-uj7m5 [amd64, arm64, ppc64el, riscv64]
- paquet virtuel fourni par liblablgtksourceview3-ocaml
-
- dep: liblablgtksourceview3-ocaml-wwfo9 [s390x]
- paquet virtuel fourni par liblablgtksourceview3-ocaml
-
- dep: libnum-ocaml-3st20 [x32]
- paquet virtuel fourni par libnum-ocaml
-
- dep: libnum-ocaml-nw4m9 [ia64]
- paquet virtuel fourni par libnum-ocaml
-
- dep: libpango-1.0-0 (>= 1.14.0) [amd64, arm64, ppc64el, riscv64, s390x]
- Mise en place et rendu de texte internationalisé
- dep: libpango-1.0-0 (>= 1.22.0) [x32]
-
- dep: libpangocairo-1.0-0 (>= 1.22.0) [x32]
- Mise en place et rendu de texte internationalisé
-
- dep: libstdlib-ocaml-2d5j3 [s390x]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libstdlib-ocaml-bdrm4 [alpha]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libstdlib-ocaml-m4xw9 [amd64, arm64, ppc64el, riscv64]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libstdlib-ocaml-rg5q2 [ia64]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libstdlib-ocaml-ye7o9 [non alpha, amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libzarith-ocaml-7dab1 [non alpha, amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par libzarith-ocaml
-
- dep: libzarith-ocaml-ap2s7 [alpha]
- paquet virtuel fourni par libzarith-ocaml
-
- dep: libzip-ocaml-3hpl7 [non amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par libzip-ocaml
-
- dep: libzip-ocaml-gm3w1 [ia64]
- paquet virtuel fourni par libzip-ocaml
-
- dep: libzip-ocaml-jmg85 [x32]
- Paquet indisponible
-
- dep: ocaml-base-4.14.1 [ia64]
- paquet virtuel fourni par ocaml-base
-
- dep: ocaml-base-5.3.0 [non amd64, arm64, ia64, ppc64el, riscv64, s390x, x32]
- paquet virtuel fourni par ocaml-base
-
- dep: ocaml-base-nox-4.11.1 [x32]
- Paquet indisponible
-
- dep: tex-common (>= 6.13)
- infrastructure commune pour construire et installer TeX
-
- dep: zlib1g (>= 1:1.1.4) [amd64, arm64, ppc64el, riscv64, s390x, x32]
- Bibliothèque de compression - binaires
-
- rec: cvc4 (<< 1.8) [x32]
- automated theorem prover for SMT problems
- ou why3-coq
- prise en charge de coq pour la plateforme de vérification why3
- ou spass
- démonstrateur automatique de théorème pour la logique du premier ordre avec égalité
- ou z3 (<< 4.8.7)
- 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
| Architecture | Version | Taille du paquet | Espace occupé une fois installé | Fichiers |
|---|---|---|---|---|
| alpha (portage non officiel) | 1.8.1-1+b1 | 21 361,9 ko | 63 926,0 ko | [liste des fichiers] |
| amd64 | 1.8.1-1+b1 | 12 092,9 ko | 43 568,0 ko | [liste des fichiers] |
| arm64 | 1.8.1-1+b1 | 13 426,6 ko | 52 363,0 ko | [liste des fichiers] |
| armel | 1.8.1-1+b1 | 21 363,5 ko | 63 923,0 ko | [liste des fichiers] |
| armhf | 1.8.1-1+b1 | 21 364,0 ko | 63 923,0 ko | [liste des fichiers] |
| hppa (portage non officiel) | 1.8.1-1+b1 | 21 364,1 ko | 63 823,0 ko | [liste des fichiers] |
| i386 | 1.8.1-1+b1 | 21 364,3 ko | 63 838,0 ko | [liste des fichiers] |
| ia64 (portage non officiel) | 1.6.0-1+b5 | 21 583,5 ko | 86 346,0 ko | [liste des fichiers] |
| loong64 (portage non officiel) | 1.8.1-1+b1 | 21 367,9 ko | 63 924,0 ko | [liste des fichiers] |
| m68k (portage non officiel) | 1.8.1-1+b1 | 21 360,3 ko | 63 827,0 ko | [liste des fichiers] |
| mips64el | 1.8.1-1+b1 | 21 364,1 ko | 63 929,0 ko | [liste des fichiers] |
| ppc64 (portage non officiel) | 1.8.1-1+b1 | 21 366,3 ko | 63 925,0 ko | [liste des fichiers] |
| ppc64el | 1.8.1-1+b1 | 12 134,8 ko | 47 242,0 ko | [liste des fichiers] |
| riscv64 | 1.8.1-1+b1 | 12 220,8 ko | 46 296,0 ko | [liste des fichiers] |
| s390x | 1.8.1-1+b1 | 12 165,2 ko | 48 688,0 ko | [liste des fichiers] |
| sh4 (portage non officiel) | 1.8.1-1+b1 | 21 363,5 ko | 63 922,0 ko | [liste des fichiers] |
| sparc64 (portage non officiel) | 1.8.1-1+b1 | 21 360,4 ko | 65 846,0 ko | [liste des fichiers] |
| x32 (portage non officiel) | 1.3.3-3 | 84 958,0 ko | 353 621,0 ko | [liste des fichiers] |