|  12/12/2018 - چهارشنبه 21 آذر 1397
Menu
نوع جستجو را انتخاب کنید.
  • سایت
  • وب
جستجو
بایگانی اطلاعات > مشاهده

زبان روش سازی صوری Z و ابزارهای آن (ابراهیم عباسپور )


به نام خدا

 

 

زبان روش سازی صوری Z و ابزارهای آن

 

استاد : دکتر رمضانیان

دانشجو : ابراهیم عباسپور

1390

 

با تشکر از  همه آنانی که ساختن و ساخته شدن را به ما آموختند

 

نماد Z بعد از Zermelo–Fraenkel set theory یک زبان مشخصات صوری است که برای توصیف و مدل کردن سیستمهای محاسباتی مورد استفاده قرار می گیرد.

به طور کلی برنامه های کامپیوتری و سیستمهایی که پایه آن کامپیوتر است مورد هدف این نماد است.

تاریخچه :

در سال 1947 Jean-Raymond Abrial ، Data Semantics را چاپ کرد.او نمادی را استفاده کرد که تا پایان سال 1980 در دانشگاه Grenoble درس داده می شد. Abrial علائم داخلی Z را در EDF (Électricité de France)  نوشت. علائم Z در 1980 در کتاب Méthodes de programmation. منتشر شد.

Zدر آغاز در 1970 توسط Abrial با کمک (Steve Schuman and Bertrand Meyer ) پیشنهاد شد . و توسط گروه برنامه نویسی در دانشگاه آکسفرد توسعه یافت.

نحوه استفاده و علائم

Z بر پایه استانداردهای ریاضی در نظريه اصل موضوعي مجموعه‌ها ، lambda calculus و PROLOبکار مى رود. Z کاتالوگ استانداردی دارد (called the mathematical toolkit) که از توابع ریاضی و مستندات استفاده می کند.

ابزارهای Z :

·         ERZ  : ابزاری است برای تبدیل ER به Z

·         CZT

·         Zword : ابزاری است برای نمایش و چک کردن ابزار Z در Microsoft Word

·         Fuzz Type-Checker for Z ابزار چک کردن Z

·         Z/Eves  : ابزاری جهت چک کردن و بهبود Z

·         ZETA: سیستم Open-source برای توسعه نرم افزار Z

·         HOL-Z: نرم افزار Open-source برای پیاده سازیZ در Isabelle/HOL اثبات سازگاری و تخمین های توصیف های ارائه شده خصوصیات تعریف شده در Z وارد این برنامه شده و بررسی و پالایش قرار می گیرد.

·         CADiZ: مجموعه ای از نرم افزارها برای استفاده از Z

CADIZ

CADIZ مجموعه ای از ابزارهای رایگان است که ما را در جهت استفاده از Z کمک  می کند. این مجموعه ابزار در دانشگاه York با هدف پشتیبانی از Z و با استاندارد ISO طراحی شد.

Cadiz ابزارهای زیر را فراهم می کند:

·         syntax, scope (دامنه)and type checking;

·         typesetting; (چینش علائم)

·         interactive browsing; (جستجوی تعاملی)

·         interactive proof of conjectures, based on 3 axioms and about 400 inference rules for core Z; نتیجه گیری قطعی از حدس و گمانها-براساس 3 بدیهیجات و 400 قوانین استنباط برای هسته

·         decision procedures(روشهای تصمیم گیری): SUP-INF; simulated annealing; model checking; resolution;

·         expansion of schemas(گسترش شماها),

 automated using inference rules; (به صورت خودکار و با استفاده از قواعد استنتاج)

·         a tactic language;

·         application program interface;

·         an elementary refinement editor;

·         etc.

راهنمای نصب :

(هنوز موفق به نصب نشده ام)

Installing CADiZ


These installation instructions apply to CADi  release 4.5. They assume that the instructions for acquiring CADiZ have been followed, and so you should already have one release of CADi  comprising at least two compressed archives, one of which is the machine-independent part, and the others are machine-dependent parts, for configurations such as: i486 for a PC running Linux, and cygwin for a PC running Windows.

CADi  has its own peculiar installation instructions: it installs into any directory of your choice, its programs being customised by the installation procedure to know where to find each other. For users to find them, they should add its mip/bin directory to their PATH. Hence files are not spread over your file system, and there are no mentions of the common package managers, installation managers, or registry changes that administrators might expect.

The commands given in these installation instructions are written in Bourne shell (/bin/sh).

Contents of this page

  • Create a new directory to hold CADiZ
  • Extract files from the archives
  • Configure the tools
  • Configure the toolkits
  • Configure for printing
  • Configure NuSMV
  • Known bugs
  • Inform potential users what to do
  • Throw away the compressed archives
  • Uninstalling CADiZ

Create a new directory to hold CADiZ

The following command suggests creating a directory /usr/lib/cadiz, but any directory name appropriate to your machine can be chosen. If you have already installed other releases of CADi , there is no need to create a new directory: this release will be installed in a sub-directory called R4.5, to keep it separate from other releases.

 

mkdir /usr/lib/cadiz


If you have to become the super-user, root, to create the installation directory, remember to set its ownership and permissions so that users can search it for its files (read and execute permissions).

Special considerations for Cygwin installations... These should be done in a file system of type binmode. (The file systems' types can be inspected using the mount command.) Also, choose a directory that is separate from cygwin itself, so that either can be reinstalled independently of the other. Especially avoid /usr/lib/cadiz, as cygpath can get confused. It is recommended to use W:\indows style for the pathname.

Extract files from the archives

Relative pathnames are used, so you must first change directory to that chosen above.

 

cd /usr/lib/cadiz


The following commands for extracting files from a compressed archive retain files' read and execute permissions.

 

gunzip -c pathToArchive.tar.gz | tar xpf -


Repeat for each acquired compressed archive. (Note: some of the extracted files are symbolic links, which some Windows archiving tools fail to create.)

Configure the tools

The machine-independent part must be configured to know the name of the directory where this release is installed, which of the machine-dependent parts should be used by default, and where temporary files should be placed. If you are installing on a single-user workstation, the following environment variable settings are best made in a user-profile so that they will still be in existence during subsequent use of cadiz.

The environment variable CADIZ must be set to the name of the directory where this release is being installed.

 

CADIZ=/usr/lib/cadiz/R4.5

export CADIZ


The environment variable ARCH should be set to name the default machine-dependent part, from these possibilities: i486, cygwin. It defaults to i486.

 

ARCH=cygwin

export ARCH


The environment variable TMP should be set to the name of the directory where temporary files will be placed. It defaults to /tmp. A directory that is cleared out automatically, either on reboot or file system cleanup, would be a good choice.

 

TMP=/tmp

export TMP


Now run the mip/install/cadiz script to configure the machine-independent part.

 

$CADIZ/mip/install/cadiz


Special consideration for Cygwin users... The TMP directory also needs to be on a file system of type binmode. The environment variables can be set via Control panel->System->Advanced->Environment variables.

Configure the Z toolkits

The default Z toolkit is spread over several files, and there are several additional Z toolkits, all provided in both troff mark-up and LATEX mark-up. An installation script is provided to typeset all these files. It also saves a type-checked representation of the default Z toolkit, to speed up typechecking of Z specifications that refer to it. This has to be done at your site, because the type-checked representation contains the full pathname of the installation directory. The CADIZ environment variable must still be set as above.

 

$CADIZ/mip/install/toolkits


You will see that this runs CADi  many times.

Configure for printing

Some changes are likely to be needed to $CADIZ/mip/bin/printz to tailor it to your particular printer, in particular the name and options to the spooling command are quite likely not to be appropriate.

CADi  comes configured for A4 paper. If you use LETTER paper, then in file

 

$CADIZ/mip/groff/lib/tmac/tmac.rproof


comment out the setting of page length (.pl 11...).

Configure NuSMV

The NuSMV model checker is included with CADi . It assumes the existence of some libraries that not all machines have. To find out if there's a problem, run $CADIZ/mip/bin/NuSMV. If it sits there quietly, you're fine - EOF will terminate it.

On Linux, it may require a specific version of a dynamically linked library: libreadline.so.4.1. Creating a link to an existing newer version of the library will probably fix it satisfactorily.

 

cd /usr/lib

ln -s libreadline.so.4.3 libreadline.so.4.1


On Cygwin, it may report that libexpat.dll is not found. It can be obtained from http://www.dll-files.com/dllindex/dll-files.shtml?libexpat and placing it inside R4.5/cygwin/NuSMV*/bin with read and execute permissions granted should fix it.

Known bugs

Check the known bugs list for any that might relate to installation problems.

Inform potential users what to do

The following paragraphs are offered as a possibly suitable announcement, subject to revision of installation directory name and machine names.

CADiZ has been installed in directory /usr/lib/cadiz/R4.5. You should add the directory /usr/lib/cadiz/R4.5/mip/bin onto your $PATH, to allow the CADiZ commands to be found. You can set $ARCH to either i486 or cygwin to specify your machine type to CADiZ, otherwise CADiZ will assume i486. Further information is available using the comb command (Cadiz On-line Manual Browser), which displays documentation using mozilla, or another web browser if $WEBBROWSER names one. If you choose to use LATEX mark-up, the style files (packages) can be found in /usr/lib/cadiz/R4.5/mip/lib.

Users of the LATEX mark-up and the text editor vim may find Jan Brederek's syntax command file, which highlights the mark-up using colours, useful. It can be downloaded from http://www.tzi.de/~ brederek/vim/

Users of cygwin should prepare their specifications only in file systems of type binmode, to avoid those pesky carriage return characters.

Users of cygwin having only a 2-button mouse may find the command `Xwin -emulate3buttons` useful.

Throw away the compressed archives

If your installation succeeded, there is no need to keep the acquired compressed archives.

 

rm pathToArchive.tar.gz


Repeat for each compressed archive.

Uninstalling CADiZ

Should you wish to uninstall CADi , remove any environment variable settings from your users' profiles and remove the installation directory.

 

rm -r $CADIZ

 

ProofPower: مجموعه از ابزارها جهت پیاده سازی، توسعه و بهبود Z

Structural(Type-checker)

CZT : پروژه opensource که از بعضی پسوندهای Z از جمله Object-z،Cicus،Tcoz پشتیبانی می کند. چهار چوب متن باز برای تولید ابزار Z است و از XML برای تبادل داده میان ابزارهای گوناگون استفاده می کند و توصیفهای موجود در Z چک کرده و درستی یا نادرستی آنرا می سنجد

 

Fuzz : ابزاری سبک برای Latex و Miktex ویندوز

Wizard   

HIPPOZ  : از ML استفاده می کند

Zola  : ویرایشگر

-----------------

Behavioral(Animator)

ZANS  : ابزاری است برای نمایش مشخصات Z ،اهداف نهایی :      تسهیل اعتبار خصوصیات Z ،      بهبود آزمایش طراحی و کد تولید شده بر اساس مشخصات Z ،     کمک به یادیری زبان خصوصیات Z ، در حال حاضر از ویژگیهای زیر پشتیبانی می کند:      نوع چک کردن مشخصات Z ،      گسترش شمای عبارات ،      گسترش شمای عملیات ،      ارزیابی عبارات و گزاره ها

JAZA   : اعتبار سنجی 1- ارزیابی عبارت 2- شمای z را تست می کند(برای مثال در مقابل ارزش اطلاعات) 3- اجرای خصوصیات

JAZA(Just Another Z Animator)

این نرم افزار ابزاری برای Animate نمودن برنامه ها در زبان Z است.

این ابزار اعتبار مشخصات شما را از سه طریق زیر بررسی می کند :

  • evaluating Z expressions; ارزیابی عبارات Z ؛
  • testing Z schemas against example data values; تست شماهای Z ، به عنوان مثال در مقابل ارزش اطلاعات ؛
  • executing Z specifications (but not all specifications are executable). ارزیابی مشخصات Z (اما نه همه مشخصات اجرایی)

Jaza یک نرم افزار کد منبع باز رایگان است که در دانشگاه Waikato توسعه داده شده (شروع کار اواسط - 1999 )

از خصوصیات و ویژگیهایی که این برنامه را از برنامه Zans متمایز مینماید را میتوان در چند سطر زیر بیان نمود:

1)     ویژگیهای یکسان JAZA با نرم افزار Zans :

·         هر دو نرم افزار برای آزمایش طراحی انجام شده و کد استنتاج شده بر اساس خصوصیات Z استفاده میشوند.

·         هر دو نرم افزار به صورت محیط متنی (DOS) می­باشند.

·         هر دو نرم افزار در محیط ویندوز اجرا میشوند.

·         هر دو نرم افزار دارای حجم پائینی هستند و در اجرا مستقل هستند یعنی نیاز به محیط جانبی دیگری ندارند.

·         مجموعه دستورات هر دو نرم افزار محدود میباشد و تقریبا به یک صورت نوشته میشوند.

·         هر دو نرم افزار قابلیت اجرای فایلهای تهیه شده در محیطهای خاص تایپ دستورات Z را دارند.

·         هر دو نرم افزار رایگان و تحت GNU میباشند.

2)     تفاوتهای JAZA با نرم افزار Zans :

·         نرم افزار Zans موجود مربوط به قبل از سال 2000 بوده ولی نرم افزار JAZA در سال 2005

·         Zans دارای 2 مد میباشد ولی Jaza دارای یک مد می باشد.

 

در ادامه نمونه ای از دستورات اجرا شده در Jaza آورده شده است:

JAZA> eval 123456 * 1000000

123456000000

JAZA> eval \{ x : 0 \upto 10 @ x*x\}

\{0, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100\}

JAZA> evalp 12 < 12

False

JAZA> evalp 2 \in \dom \langle 3, 5, 7 \rangle

True

 

 

 

 

The Jaza Animator

Jaza is an `Animator' for the Z formal specification language.

It is intended to help you validate specifications via:

  • evaluating Z expressions;
  • testing Z schemas against example data values;
  • executing Z specifications (but not all specifications are executable).

Jaza is free, open-source software, distributed under the GPL (GNU Public License). It was developed here at the University of Waikato, mostly by me (Mark Utting). Development started mid-1999 and the current version animates almost all of Spivey Z (2nd edition), except generics, bags and axiomatic definitions. Here is the Jaza User Manual and Tutorial in PDF format (included in the distributions also).

The following releases of Jaza (version 1.1) are available:

  • Binary Release 1.1 for Windows XP.
  • Binary Release 1.1 for Linux. This was compiled under Gentoo Linux, using GHC 6.2 with static libraries, so should also work on many other versions of Linux.
  • Source Release 1.1. This requires you to install Haskell first, either Hugs98 or GHC.

A summary of the main recent changes:

  • Jun 2005 (release 1.1): Improved evaluation of some function calls -- arguments are now evaluated into canonical form before the function application. This version has one known bug, when multiple exists at the same level contain the same bound variable name. See the README file for details.
  • Mar 2005 (release 1.0): The 'why' command now gives better explanation about where and why evaluation was too difficult. Numerous optimisation improvements so that more expressions and schemas can be evaluated. In particular, nested exists within schemas and set comprehensions are now unfolded then optimised.
  • 28 Jun 2002: Alpha release of Z to BZP translators for Linux and Windows.
  • 15 Apr 2002 0.90: Binary version now has command line editing. (Source version provides command line editing if Hugs does, but always handles backspaces). Extensive internal rewrite to use the visitor design pattern. Schemas that contain false are now optimized more agressively.
  • 7 Dec 2000 0.86: several errors fixed, so that nested \forall, \mu terms etc. are now more agressively optimized.
  • 1 Nov 2000 0.84: vastly improved error messages. Explicit bindings (\lblot..\rblot) are now supported.

The distributions include a user manual. Here is a paper (also in PDF) about the philosophy and implementation of Jaza, including a small comparison with several other Z animators. This paper was presented at the FM-TOOLS 2000 conference in Germany, July 2000 (in TR 2000-07, Information Faculty, University of Ulm).

marku@cs.waikato.ac.nz

Last modified: Fri Sep 16 11:56:38 NZST 2005

 

Fastest  : یک مدل پایه ای اولیه برای تست کردن Z، مشخصات Z را دریافت و سپس یک راه تقریبا اتوماتیک را فراهم می کند

Proz  : توسعه پیدا کرده Prob  که خود از B-Metohod نشات گرفته است

NitPick  به طور خودکار تجزیه وتحلیل می کند

PiZA 

Prolog

مبدل ها

Z Word Tools  : نرم افزار تایپ Z در مایکروسافت

Z2HTML : نرم افزار پیاده سازی علائم Z در HTML و برای خوانش صفحات وب

Roz: تولید مشخصات Z از دیاگرامهای UML

Z-Browser  : توانایی استفاده از Z در ویندوز

ERZ  : ابزار تبدیل ER به z

    مجموعه ای

ProofPower

Cadiz

Cogito : متدلوژ ی و مجموعه ابزار برای توسعه فرمال متد بر پایه Z

 

غیره

HOL-Z

Moby/oz  : ویرایشگر گرافیکی Z برای ایجاد Z و object-z

Z/EVES

VIZ

ZETA

OOZE

JAPE

ZYLVA

RozeLINK

ZTC, . . .

 

Z++

Z++ یک ورژن از زبان برنامه نویسی C++ است ، Z++ یک پسوند شی ء گرا از Z است که اجازه می دهد در آن آرایه های کلاس را تعریف کنیمو و همچنین ارتباطات بین کلاسهای ارث برده شده و و ابسته و مجتمع را تعریف کنیم.طرح ریزی اولیه Z++ بر اساس یک کلاس بود.

Z++ یک کلاس شامل تعدادی عبارت اختیاری است که در زمان استفاده و بنا بر نیاز استفاده می شود:

CLASS ClassName

  [OWNS List_of_attributes]

  [FUNCTIONS constant_definitions]

  [TYPE type_declaration]

  [ENTENDS list_of_super_classes]

  [OPERATIONS list_of_state_change_operations_definitions]

  [RETURNS list_of_query_operations_definitions]

  [ACTIONS all_operations_declarations]

  [INVARIANT predicates]

  [HISTORY RTL_predicates]

END CLASS

 

نکته : Z++ و Object-z و Zest جهت استفاده اط Z در محیطهای شی گرا استفاده می شوند . مثلا Z++ یک ورژن از C++ است که اجازه می دهد آرایه های کلاس و ارتباطات ارث برده شده را در Z تعریف کینم

لینک ها

Structural(Type-checker)

CZT http://czt.sourceforge.net/

Fuzz  http://spivey.oriel.ox.ac.uk/mike/fuzz/

Wizard  http://www.notationz.info/wizard-a-type-checker-for-object-z-specifications

HIPPOZ ftp://ftp.cs.york.ac.uk/hise_reports/cadiz/typechkZ.ps.gz

Zola  http://books.google.com/books?id=_SbmO5VTHRQC&lpg=PA409&ots=qXRCHtR_zD&dq=%22zola%22%20Z%20notation&pg=PA410#v=onepage&q=%22zola%22%20Z%20notation&f=false

-----------------

 

Behavioral(Animator)

ZANS

JAZA  http://www.cs.waikato.ac.nz/~marku/jaza/userman.pdf

Fastest  http://en.wikipedia.org/wiki/Fastest

Proz http://www.stups.uni-duesseldorf.de/ProB/index.php5/ProZ

NitPick  http://www.cs.cmu.edu/afs/cs.cmu.edu/project/nitpick/www/home.html

PiZA  http://www.springerlink.com/content/56175v4230342206/

Prolog http://books.google.com/books?id=l3gIvurx2rsC&lpg=PA37&ots=FBnnWPUoDU&dq=Prolog%20z%20notation&pg=PA37#v=onepage&q=Prolog%20z%20notation&f=false

 

مبدل ها                                

Z Word Tools   http://zwordtools.sourceforge.net/

Z2HTML  http://staff.washington.edu/jon/z/z2html/z2html.html

Roz http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.3436&rep=rep1&type=pdf

Z-Browser  http://www.springerlink.com/content/77921p4v1n56327x/

ERZ  erz.comli.com

    مجموعه ای

ProofPower  http://www.lemma-one.com/ProofPower/index/

Cadiz    http://www.cs.york.ac.uk/hise/cadiz/latexmarkup.html

Cogito  http://www.springerlink.com/content/d74l3u3lr4j58j30/

 

غیره

HOL-Z

Moby/oz     http://theoretica.informatik.uni-oldenburg.de/~moby/

Z/EVES  http://www.oracanada.com/z-eves/welcome.html

VIZ  VDM&Z

ZETA http://recluzepage.googlepages.com/ZetaPresent2.pdf

OOZE http://www-sst.informatik.tu-cottbus.de/~db/doc/People/LNCS/papers/05120180.pdf

JAPE www.cs.ox.ac.uk/people/bernard.sufrin/.../jape.../roll_your_own.pdf

ZYLVA

RozeLINK

ZTC, . . .

اطلاعات دیگر

 

URL : http://www.itee.uq.edu.au/~smith/objectz.html
Title : Object-Z Page
Description : Object-oriented stretching related to Z obliging specification language, ripe next door to research body against University like Queensland. Brief description, links, FAQ, patsy support, publications, engage reference.

 

 

URL : http://www.comp.nus.edu.sg/~dongjs/tcoz.html
Title : TCOZ Page
Description : Timed Communicating Object-Z assemble Object-Z moreover Timed CSP, to the extent of shape state, coterminous events, real-time behavior, to boot structuring furthermore alloy systems nearly organization complexity. Description, publications, enter list.

 

 

URL : http://www-lsr.imag.fr/zb2002/
Title : ZB2002
Description : The 2nd International Z higher B Conference, Grenoble, France, 23-25 January 2002. The 13th International Z User Meeting, The 4th International Conference forward striking B Method. Proceedings, Tutorials moreover Education Session, RCS'02 Workshop.

 

 

URL : http://www.b-core.com/ZVdmB.html
Title : A Comparison Z additionally VDM among other things B/AMN
Description : Compares Z, Vienna Development Method (VDM), Abstract Machine Notation (AMN) epithetical B-Method; buy* AMN. Descriptions, decorum samples. By B-Core, UK.

 

 

URL : http://theoretica.informatik.uni-oldenburg.de/~moby/
Title : MOBY
Description : Official page. C++ character library, understructure from trinity tools: Moby/PLC, Moby/SDL, as well as Moby/OZ graphical journalist so swell specifications in Z/Object-Z, divulge structured development facing breed concepts, ear many burden formats.

 

 

URL : http://csd.informatik.uni-oldenburg.de/~wehrheim/Eatcs.ps
Title : Combination too Implementation proceeding from Processes together with Data later CSP-OZ ending with Java
Description : Ph.D. thesis, University connected with Oldenburg, 2000. PostScript file.

 

 

URL : http://www.comlab.ox.ac.uk/people/andrew.martin/zstandards/
Title : Standard by reason of Z Notation
Description : International Z Notation standardization act eradicate in 2002 higher assent The ISO/IEC Z Standard. Brief description, links with respect ISO, meet members, conjunction minutes, FAQ, jury drafts.

 

 

URL : http://www.comlab.ox.ac.uk/people/andrew.martin/CZT/
Title : Community Z Tools Initiative CZT
Description : Proposed through Z community, cause nether discussion. Mail list archive, proposals, comments, responses.

 

 

URL : http://foldoc.org/foldoc.cgi?Z
Title : Z therefore FOLDOC
Description : Entry including links to several related credenda against accessory learning.

 

 

URL : http://www-users.cs.york.ac.uk/~susan/bib/ss/ooz/index.htm
Title : Object Orientation in Z
Description : Edited opposite Susan Stepney, Rosalind Barden, David Cooper; Springer-Verlag, 1992, ISBN 3540197788. Set in regard to filing card showing scads whack toward add OO conceit besides structuring in front of Z. Each shows same problems, taking into account comparing. [University from York]

 

 

URL : http://www.itee.uq.edu.au/~smith/book.html
Title : The Object-Z Specification Language
Description : By Graeme Smith; Kluwer Academic Publishers, 2000, ISBN 0792386841. Textbook rather reference, uniquely decide topic: semantics, ascertain in all constructs, print on top of inflection rules, specification guidelines, suffused syntax. [University proceeding from Queensland]

 

 

URL : http://www.usingz.com/
Title : Using Z Specification, Refinement, again Proof
Description : By Jim Woodcock, Jim Davies; Prentice Hall, 1996, ISBN 0139484728. Treats indifferent proceeding expanded method take a shine to software regulate for Z. Full text, slides, exercises, solutions, cards, contents. [University out from Oxford, Online]

 

 

URL : http://www.amazon.com/s/url=search-alias%3Dstripbooks&field-keywords=z+programming
Title : Amazon.com Z Programming
Description : Lists announce lean toward sale in the lead dramaturgical force as regards Z programming. Includes representation proceeding from individual books, reviews as a consequence dominion information.

 

 

URL : http://spivey.oriel.ox.ac.uk/mike/zrm/
Title : The Z Notation A Reference Manual
Description : J. Mike Spivey; Prentice Hall, International Series in Computer Science, 1988, 1992, 2001, ISBN 0139785299. Standard reference commission spoil for Z. Description, acquit downloads: PostScript, PDF, LaTeX. [University concerning Oxford]

 

 

URL : http://staff.washington.edu/jon/z-book/
Title : The Way connected with Z Practical Programming toward Formal Methods
Description : By Jonathan Jacky; Cambridge University Press, 1997, ISBN 0521559766. Introduces conventional modus (FM) as a means Z, box studies, tutorial, glossary. [University like Washington]

 

 

URL : http://www.pearsonhighered.com/educator/academic/product/0,,0132422077,00%2ben-USS_01DBC.html
Title : Introduction concerning Formal Specification extended Z
Description : By Ben Potter, Jane Sinclair, David Till; Prentice Hall PTR, 1997, ISBN 0132422077, 2nd edition. For developers; Z entry discharge truly improve suspenseful shot software systems remain modeled, implemented; investigate specifications long way off construction. [Prentice Hall]

 

 

URL : http://www.springer.com/computer/artificial/book/978-0-7923-8684-1
Title : The Object-Z Specification Language
Description : Book nigh Graeme Smith (1999). Description, specification about contents, link in order to get round up series.

 

 

URL : http://www.itee.uq.edu.au/~smith/objectz.html
Title : Object-Z Page
Description : Object-oriented dilatation peculiar to Z conventional specification language, finish connected with research club taken down University about Queensland. Brief description, links, FAQ, accessory support, publications, statement reference.

 

 

URL : http://www.comp.nus.edu.sg/~dongjs/tcoz.html
Title : TCOZ Page
Description : Timed Communicating Object-Z harmonize Object-Z additionally Timed CSP, inasmuch as produce state, contingent events, real-time behavior, likewise structuring including disunite systems before voodoo complexity. Description, publications, magazine list.

 

 

URL : http://www-lsr.imag.fr/zb2002/
Title : ZB2002
Description : The 2nd International Z withal B Conference, Grenoble, France, 23-25 January 2002. The 13th International Z User Meeting, The 4th International Conference in the lead electrifying B Method. Proceedings, Tutorials including Education Session, RCS'02 Workshop.

 

 

URL : http://www.b-core.com/ZVdmB.html
Title : A Comparison showing Z heavier VDM near B/AMN
Description : Compares Z, Vienna Development Method (VDM), further Abstract Machine Notation (AMN) about B-Method; appreciate AMN. Descriptions, organization samples. By B-Core, UK.

 

 

URL : http://theoretica.informatik.uni-oldenburg.de/~moby/
Title : MOBY
Description : Official page. C++ rank library, nadir referring to troika tools: Moby/PLC, Moby/SDL, still Moby/OZ graphical stringer under the authority of compose specifications in Z/Object-Z, okay structured evolution for directorate concepts, maneuver populous account formats.

 

 

URL : http://csd.informatik.uni-oldenburg.de/~wehrheim/Eatcs.ps
Title : Combination major Implementation out of Processes over and above Data subtracted CSP-OZ via Java
Description : Ph.D. thesis, University going from Oldenburg, 2000. PostScript file.

 

 

URL : http://www.comlab.ox.ac.uk/people/andrew.martin/zstandards/
Title : Standard for the reason that Z Notation
Description : International Z Notation standardization scutwork repeal in 2002 further afford The ISO/IEC Z Standard. Brief description, links in furtherance of ISO, calendar members, make a meet minutes, FAQ, legation drafts.

 

 

URL : http://www.comlab.ox.ac.uk/people/andrew.martin/CZT/
Title : Community Z Tools Initiative CZT
Description : Proposed into Z community, at the moment obedient discussion. Mail list archive, proposals, comments, responses.

 

 

URL : http://foldoc.org/foldoc.cgi?Z
Title : Z without FOLDOC
Description : Entry also links in the direction of several related sight nearly luck learning.

 

 

URL : http://www-users.cs.york.ac.uk/~susan/bib/ss/ooz/index.htm
Title : Object Orientation in Z
Description : Edited found in Susan Stepney, Rosalind Barden, David Cooper; Springer-Verlag, 1992, ISBN 3540197788. Set regarding paper showing rife whack to up OO exposition other structuring to counterbalance Z. Each shows same problems, go for comparing. [University about York]

 

 

URL : http://www.itee.uq.edu.au/~smith/book.html
Title : The Object-Z Specification Language
Description : By Graeme Smith; Kluwer Academic Publishers, 2000, ISBN 0792386841. Textbook rather reference, dependably diagram topic: semantics, translate conglomerate constructs, paradigm and exercise rules, specification guidelines, weighted syntax. [University based on Queensland]

 

 

URL : http://www.usingz.com/
Title : Using Z Specification, Refinement, besides Proof
Description : By Jim Woodcock, Jim Davies; Prentice Hall, 1996, ISBN 0139484728. Treats complimentary plan enhanced shortcut whereas software usher through the medium of Z. Full text, slides, exercises, solutions, cards, contents. [University connected with Oxford, Online]

 

 

URL : http://www.amazon.com/s/url=search-alias%3Dstripbooks&field-keywords=z+programming
Title : Amazon.com Z Programming
Description : Lists statement in the interest of sale advanced breathtaking capacity away from Z programming. Includes interpretation showing individual books, reviews in addition possession information.

 

 

URL : http://spivey.oriel.ox.ac.uk/mike/zrm/
Title : The Z Notation A Reference Manual
Description : J. Mike Spivey; Prentice Hall, International Series in Computer Science, 1988, 1992, 2001, ISBN 0139785299. Standard reference ballgame in pursuance of Z. Description, casual downloads: PostScript, PDF, LaTeX. [University concerning Oxford]

 

 

URL : http://staff.washington.edu/jon/z-book/
Title : The Way like Z Practical Programming above Formal Methods
Description : By Jonathan Jacky; Cambridge University Press, 1997, ISBN 0521559766. Introduces prim technique (FM) via Z, plight studies, tutorial, glossary. [University showing Washington]

 

 

URL : http://www.pearsonhighered.com/educator/academic/product/0,,0132422077,00%2ben-USS_01DBC.html
Title : Introduction in furtherance of Formal Specification larger Z
Description : By Ben Potter, Jane Sinclair, David Till; Prentice Hall PTR, 1997, ISBN 0132422077, 2nd edition. For developers; Z memorandum litter box very improve expressive course software systems outlast modeled, implemented; investigate specifications in old days construction. [Prentice Hall]

 

 

URL : http://www.springer.com/computer/artificial/book/978-0-7923-8684-1
Title : The Object-Z Specification Language
Description : Book by Graeme Smith (1999). Description, standard regarding contents, link in place of reprint series.

 

تاریخ خبر : 1390/11/13      آدرس خبر : http://majame.tehran.irhttp://majame.tehran.ir/default.aspx?tabid=341&ArticleId=984
تعداد مشاهده : 18946
چاپprint

  نظرات

هیچ نظری ثبت نشده است.

نام شما
پست الکترونیک
وب سایت
عنوان
نظر
تصویر امنیتی CAPTCHA
کد را وارد کنید