![[Top]](/archive/z/z.gif)
Virtual Library
Génie Logiciel
Langages
Méthodes Formelles
forms interactives (si votre client WWW le permet):
Envoyer un mail à Jonathan.Bowen@comlab.ox.ac.uk si vous connaissez des informations on-lines relatives à Z qui ne sont pas ici. Utiliser le newsgroup comp.specification.z newsgroup (accessible par email à zforum@comlab.ox.ac.uk) pour les questions générales.
Z est maintenant utilisé dans l'industrie dans les développements logiciels (et matériels) en Europe et aux USA. Une standardisation internationale est à l'étude sous l' ISO/IEC JTC1/SC22 WG19 sur les langages de spécifications au Royaume-Uni . L'utilisation de Z a obtenu au Royaume-Uni le Queen's Award for Technological Achievement en 1992 pour son utilisation dans le projet IBM CICS et à contribuer à celui de 1990 pour son utilisation pour spécifier le standart de IEEE pour l'arithmétique des flottants. ( voir Technical Monograph PRG-58).
Il y a en plus de nombreux OUCL Technical Monographs (Mémoires) et Technical Reports(rapports techniques) sur Z.
Une discussion par mail sur la méthode SAZ (un mélange de méthode SSADM et de Z) existait mais elle est désormais terminée.
D'autres newsgroups relatifs à des sujets comparables existent: comp.specification, comp.software-eng et comp.risks qui est modéré (voir ici pour les groupes comp ). Les Mettings des utilisateurs de Z sont aussi annoncés dans les news.announce.conferences .
Les archives de Z contiennent une bibliographie BibTeX sur Z-donnant les publications qui sont disponibles comme rapport techniques publiables Select Z Bibliography. Cette bibliographie est aussi disponible dans un format standartisé. Un liste de livres régulièrement mise à jour est aussi disponible. La FACS Europe newsletter includes Z-related material.
Si vous voulez des informations sur les publications faites au PRG comme Technical Monographs (en particulier , voir PRG-46, PRG-47, PRG-48, PRG-49, PRG-50, PRG-58, PRG-60, PRG-61, PRG-62, PRG-63, PRG-68, PRG-74, PRG-81, PRG-101, PRG-103, PRG-107 qui parlent de Z) et des rapports techniques (dont beaucoup parlent de la notation ), contactez le documentaliste de l'OUCL.
La principale partie et les annexes du draft Z Base Standard (version 1.0) sont disponibles. Une version imprimée de Z Base Standard est disponible comme Technical Monograph du PRG PRG-107). Pour de plus amples informations sur le Z Base Standard, contactez John Nicholls or Stephen Brien. De nouvelles informations concernant la standardisation vont lorsqu'elles seront disponibles. Voir aussi les informations la standardisation par Andrew Martin.
Une étude sur les méthodes formelles comprend de vrais exemples de Z dans des cas industriels.
Un Glossaire de Z est aussi disponible.
La dernière conférence des Utilisateurs de Z (ZUM'94) s'était tenu les 29 et 30 Juin 1994 au St. John's College à Cambridge, Rouaume Uni. Les conférences sont organisées en association avec BCS FACS et sont supportés par un ProCoS-WG Working Group du ESPRIT comme un de ses open meetings. Des copies des affiches sont encore disponibles . Les conférenciers invités étaient David Garlan (CMU), Mike Gordon (Cambridge), Leslie Lamport (DEC SRC), Jim Woodcock (Oxford), Robert Worden (Logica), and Maurice Wilkes (Olivetti) . Les informations sur les proceedings de ZUM'94 et un rapport sur le meeting sont accéssibles. Des tutoriaux étaient soutenus lors des 2 jours précédent le meeting et un session spéciale au sujet de l'enseignement avait eu lieu le 1er Juillet 1994.
Les Z publications précédentes des Z User Meeting ont été publiées par Springer- Verlag dans leur collection: Workshops in Computing depuis 1989 . Celles d'avant avaient été publiées par le Oxford University Computing Laboratory et les principales parties de meetings de 1987 et 1988 sont disponibles.
Le prochain meeting est programmé pour le printemps 1997 à City Univerity , London.
D'autres informations sur des meetings s'apparentant sont disponibles ailleurss. Voir aussi la listes des actualités des méthodes formelles .
Il existe un vérificateur de type appelé fuzz vendu avec fuzz.sty , un fichier de style LaTeXqui a de plus belles fontes et plus de symboles. Contactez Mike Spivey et/ou regardez la fuzz order form. La vérificateur de type tourne actuellement sous Sun 3, Sun 4, IBM PC et VAX/VMS .
oz.sty, une version étendue de zed.sty pour Z et sa version orientée object Object-Z crée par Paul King king@batserver.cs.uq.oz.au of University of Queensland, Australia, un document explicatif est aussi disponible au format LaTeX ou PostScript . Une version pour LaTeX2e est aussi disponible. oz.sty doit être généré par oz.dtx avec oz.ins. Un guide et un fichier de test sont aussi lisibles.
csp_zed.sty est un fichier de style dérivé de zed.sty par Jim Davies (anciennement au OUCL, maintenant à l' University of Reading, UK) qui supporte CSP (Communicating Sequential Processes) et Z, et utilise les nouvelles fontes . zed-csp.sty a été développé après pour pouvoir travailler avec LaTeX2e, disponible avec de la documentation .
CADiZ fournit un support pour Z en utilisant soit troff soit LaTeX , il est développé à York. Une description est disponible.
Le système de démonstration automatique de théorèmes HOL basé sur un logique d'ordre supérieure fournit des outils pour l'utilisation de Z comme on peut le voir dans le document Z and HOL. Des spécifications en Z traitées en Hol sont disponibles par FTP.
ProofPower, an industrial strength Z theorem prover based on Higher Order Logic, is available from ICL. Contact ProofPower-support@win.icl.co.uk for further information. See also some brief information on proof infrastructure for Z using HOL.
ZTC est un vérificateur de type pour Z pour PC sous DOS, Sun 4 et Sun sous Solaris fournis au format Unix tar . Un guide est disponible ZTC est disponible pour l'enseignement ou pour une utilisation non commerciale. Il fait partie d'un projet de recherche pour le développement des outils pour Z. Contactez Xiaoping Jia ( jia@cs.depaul.edu ) pour plus d'informations.
Le vérificateur de type ZTC pour PC est disponioble avec quelques informations. Hippo, un vérificateur de type de Z de Bernard Sufrin fait en ML est aussi disponible.
JAPE (Just Another Proof Editor) par Bernard Sufrin et Richard Bornat supporte la théorie des ensembles (Z).
Les travaux sont réalisés pour ajouter des extensions mathématiques au format HTML+ et inclure les notations de Z par les clients WWW. Contactez Phillip M. Hallam-Baker à hallam@alws.cern.ch si vous intéressé. Voir aussi, des informations au OUCL.
Différentes fontes TrueType pour Z sous MS Windows sous disponibles (au format pkzip ):
Les développeurs d'outils peuvent trouver la syntaxe de Z , créé à partir d'échantillons description de syntaxe in general as part of the MATHS Project. See also MATHS source Z syntax.
Une Z grammaire expérimentale pour l'utilisation de PRECC compiler-compiler est disponible surtout sous Unix mais aussi sous DOS.
Une démonstration d'un Z Browser est disponibles pour des PC sous Windows .
Voir aussi La Base de Données des Méthodes Formelles (second sourced) maintainue par Tim Denvir, elle comporte la description de plusieurs méthodes dérivées de Z.
VDM a aussi une mailing list appelé VDM FORUM (non modéré) . Envoyer un email contenant ``join vdm-forum nom'' où ``nom'' est votre vrai nom à mailbase@mailbase.ac.uk. Pour contacter le responsable de la liste , écrivez à John Fitzgerald , University of Newcastle, vdm-forum-request@mailbase.ac.uk. Voir aussi d'autres informations sur VDM.
Voir aussi la Méthode B pour le développement de logiciels à l'aide de méthodes formelles.
Traduit de l'anglais par
Jean-Philippe Cottin,
équipe Logiques, Langages et Spécifications,
Ecole Nationale Supérieure des
Télécommunications
17 Juillet 1995.
Comments,
corrections and new information are gratefully received.
Part of the OUCL
archive.
See also information on other
formal methods and
notations.