Yazılım geliştirebilmenin formal metodları o yazılım tanımlamasının geçerliliğine bağlıdır. Böyle bir tanımlama genelde 'Z' gibi bir formal dilde ifade edilir. A ncak, geçerli olması için, 'Z' tanımlaması test edilmeli, bunu yapabilmek için de anim asyon yapılabilecek ve icra edilebilecek bir forma transfer edilebilmelidir. 'Z' tanımlamalarının animasyonları için kullanılan dillerden birisi Prolog'dur. Bu makalede 'Z' şemalarını Prolog'a çeviren teknikler açıklanmaktadır.Aym zamanda bu tür bir çevirmenin eksikleri ve belirsizlikleri üzerinde durulacaktır

Anahtar Kelimeler:

form al metodlar, Z ' tanımlama dili, animasyon, Z ' şeması

ANIMATION OF Z SPECIFICATIONS BY TRANSLATION TO PROLOG

Formal methods of software development rely on the validation of the specification of the software. Such specification is normally expressed in a formal language such as Z. However, in order to be validated the Z specification must be tested, and to achieve this it has to be transformed into a form that can be executed or animated. Prolog was one of the languages used for animation of Z specifications. This paper explains the techniques used for translating Z schemas into Prolog predicates. It also examines some of this translation shortcomings and unreliable features.

Keywords:

Formal Methods, Z Specification, Animation, Z Schema,

PDF

___

ANDREW, S. and Norcliffe, A. (1990), "A CASE Tool for Demonstrating Z specifications", Proc. IEE Colloquium on Application o f CASE Tools IEE, London.
BARDEN, R.; Stepney, S. and Cooper, D. (1994), Z in Practice, Prentice-Hall.
BERG, H. K.; Boebert W. E.; Franta, W. R. and Moher, T. G. (1982), Formal methods o f program Verification and specification, Prentice-Hall Inc.
BLOOMFIELD, R. E. and Froome, P. K. D. (1986), "The Application of Formal Methods to the Assessment of High Integrity Software", IEEE Trans., SE-12(9), 988-993.
BOEHM, B. K. (1979), "Software engineering: R & D trends and defence needs", Research Directions in software Technology, M.I.T Press, 44-86
BURKE, E. and Foxley ,E. (1996), Logic and its Applications, Prentice Hall International Series in Computer Science.
CLOCKSIN, W. F. and Mellish, C. S. (1994), Programming in Prolog , SpringerVerlag.
DEVILLE, Y. (1990), Logic Programming - Systematic Program Development, Addison-Wesley Pub. Co.
DICK, A. J.; Kraus, P. J. and Cozens, J. (1990), "Computer AidedTransformation of Z into Prolog", Proc. Fourth Annual Z Users Meetings 1989 , Workshops in Computing: Springer-Verlag, Oxford, 71-85.
DIJKSTRA, E. G. (1979), "Structured Programming", Classics in Software Engineering, Yourdon Press.
DILLER, A. (1990), Z: A n Introduction to Formal M ethods, John Wiley, UK.
FIELDS, B. and Elovang-Goransson, M. (1992), "AVDM Case Study in mural", IEEE Trans. Software Eng., 18(4), 279-295.
Futatsugi, K.; Goguen, J. A.; Jouannaud, J. P. and Meseguer, J. (1985), "Principles of OBJ2", Proc. 12th A C M Sym posium on Principles o f Programming Languages, New Orleans, 52-66.
Gladden, G. R. (1982), "Stop the Life-cycle, I Want to Get Off", A C M SIGSOFT Soft. Eng. Notes, 7(2), 35-39.
Goguen, J. A. (1984), "Parameterized Programming", IEEE Trans. Software E n g , 10(5), 528-543.
Guttag, J. V. and Horning, J. J. (1978), "The Algebraic Specification of Abstract Data Types", Acta Inform , 10, 27-52.
Hatcher, W. S. (1982), The logical Foundations o f M athematics, Pergamon Press, Canada.
Hayes, I. J. and Jones, C. B. (1991), "Specifications are not (Necessarily) Executable", IEE Software Engineering J ., 330-338.
Hekmatpor, S. and Ince, D. (1988), Software Prototyping, Formal Methods and VDM, Addison-Wesley.
Henderson, P. and Minkowitz, C. (1985), "The 'me too' method of software design", Technical Report FPN-10, University of Stirling, Dept. of Computer Science.
Hewitt, M. A.; O'Halloran, C. M. and Sennett, C. T. (1997),"Experiences with PiZA, an Animator for Z", Proc. 11th Annual Z Users Meetings, Workshops in Computing: Springer-Verlag, LNCS 1212.
Hogger, C. (1984), Introduction to logic programming, Academic Press, London,
Jalote, P. (1989), "Testing the completeness of Specifications", IEEE Transaction on software engineering , 15(5), 526-531.
Jones, C. B. (1986), Systematic Software Development Using VDM, PrenticeHall, London.
Kemmerer, R. A. (1985), "Testing Formal Specifications to Detect Design Errors", IEEE Trans. Software Eng., 11(1), 32-43.
Knott, R. D. and Kraus, P. J. (1988), "An Approach to Animating Z Using Prolog", Report A1.1, Alvey Project SE/065, University of Surrey.
Kowalski, R. A. (1979), Logic fo r problem solving, North-Holland, New York.
Lloyd, J. W. (1984), Foundations o f Logic Programming, Springer-Verlag, New York.
MoD UK (1991), "The Procurement of Safety Critical Software in Defence Equipment", Defence Standard 00-55/Issue1, UK Ministry of Defence.
Moore, R. C. (1982), The Role o f Logic in Intelligent Systems SRI International.
Ross, P. (1989), Advanced Prolog, Addison-Wesley Pub. Co.
Spivey, J. M. (1989), The Z Notation: a Reference Manual, Prentice-Hall.
Stepney, S. and Lord, S. P. (1987), "Formal Specification of an Access Control System", Software-Practice and Experience, 17(9), 575-593.
Turner, D. (1986), "An Overview of Miranda", A C M SIG PLAN Notices21(12), 158-166.
West, M. M. and Eaglestone, B. M. (1992), "Software development: two approaches to animation of Z specification using Prolog", Software Engineering, 7(4), 264-276.
West, M. M. (1988), Z/PROLOG Translator, M.Sc. Dissertation, University of Bradford.
Wordsworth, J. B. (1996), Software Engineering with B, Addison-Wesley.
Zin, A. M. (1993), ZFDSS: A Formal Development Support System Based on the Liberal Approach, Ph.D. Thesis, Dept. of Comp. Science, University of Nottingham, UK.

ISSN: 1302-6739
Yayın Aralığı: Yılda 2 Sayı
Başlangıç: 2000
Yayıncı: Doğuş Üniversitesi

Arşiv