Abstract

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

Keywords

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

ANIMATION OF Z SPECIFICATIONS BY TRANSLATION TO PROLOG

Abstract

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

References

1. ANDREW, S. and Norcliffe, A. (1990), "A CASE Tool for Demonstrating Z specifications", Proc. IEE Colloquium on Application o f CASE Tools IEE, London.
2. BARDEN, R.; Stepney, S. and Cooper, D. (1994), Z in Practice, Prentice-Hall.
3. 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.
4. 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.
5. BOEHM, B. K. (1979), "Software engineering: R & D trends and defence needs", Research Directions in software Technology, M.I.T Press, 44-86
6. BURKE, E. and Foxley ,E. (1996), Logic and its Applications, Prentice Hall International Series in Computer Science.
7. CLOCKSIN, W. F. and Mellish, C. S. (1994), Programming in Prolog , SpringerVerlag.
8. DEVILLE, Y. (1990), Logic Programming - Systematic Program Development, Addison-Wesley Pub. Co.

9. 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.
10. DIJKSTRA, E. G. (1979), "Structured Programming", Classics in Software Engineering, Yourdon Press.
11. DILLER, A. (1990), Z: A n Introduction to Formal M ethods, John Wiley, UK.
12. FIELDS, B. and Elovang-Goransson, M. (1992), "AVDM Case Study in mural", IEEE Trans. Software Eng., 18(4), 279-295.
13. 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.
14. Gladden, G. R. (1982), "Stop the Life-cycle, I Want to Get Off", A C M SIGSOFT Soft. Eng. Notes, 7(2), 35-39.
15. Goguen, J. A. (1984), "Parameterized Programming", IEEE Trans. Software E n g , 10(5), 528-543.
16. Guttag, J. V. and Horning, J. J. (1978), "The Algebraic Specification of Abstract Data Types", Acta Inform , 10, 27-52.
17. Hatcher, W. S. (1982), The logical Foundations o f M athematics, Pergamon Press, Canada.
18. Hayes, I. J. and Jones, C. B. (1991), "Specifications are not (Necessarily) Executable", IEE Software Engineering J ., 330-338.
19. Hekmatpor, S. and Ince, D. (1988), Software Prototyping, Formal Methods and VDM, Addison-Wesley.
20. Henderson, P. and Minkowitz, C. (1985), "The 'me too' method of software design", Technical Report FPN-10, University of Stirling, Dept. of Computer Science.
21. 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.
22. Hogger, C. (1984), Introduction to logic programming, Academic Press, London,
23. Jalote, P. (1989), "Testing the completeness of Specifications", IEEE Transaction on software engineering , 15(5), 526-531.
24. Jones, C. B. (1986), Systematic Software Development Using VDM, PrenticeHall, London.
25. Kemmerer, R. A. (1985), "Testing Formal Specifications to Detect Design Errors", IEEE Trans. Software Eng., 11(1), 32-43.
26. 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.
27. Kowalski, R. A. (1979), Logic fo r problem solving, North-Holland, New York.
28. Lloyd, J. W. (1984), Foundations o f Logic Programming, Springer-Verlag, New York.
29. MoD UK (1991), "The Procurement of Safety Critical Software in Defence Equipment", Defence Standard 00-55/Issue1, UK Ministry of Defence.
30. Moore, R. C. (1982), The Role o f Logic in Intelligent Systems SRI International.
31. Ross, P. (1989), Advanced Prolog, Addison-Wesley Pub. Co.
32. Spivey, J. M. (1989), The Z Notation: a Reference Manual, Prentice-Hall.
33. Stepney, S. and Lord, S. P. (1987), "Formal Specification of an Access Control System", Software-Practice and Experience, 17(9), 575-593.
34. Turner, D. (1986), "An Overview of Miranda", A C M SIG PLAN Notices21(12), 158-166.
35. 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.
36. West, M. M. (1988), Z/PROLOG Translator, M.Sc. Dissertation, University of Bradford.
37. Wordsworth, J. B. (1996), Software Engineering with B, Addison-Wesley.
38. 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.