ANNA A Language for Annotating Ada Programs

این راهنمای مرجع ANNA جلد دیگری است که به جامعه ADA خطاب شده است. ANNA یک توسعه زبان ADA است که شامل امکاناتی برای تعیین رسمی رفتار مورد نظر برنامه های ADA می شود. این برنامه برای برآورده کردن نیاز درک شده برای تقویت ADA با حاشیه نویسی های دقیق قابل پردازش توسط ماشین طراحی شده است تا بتوان روش های رسمی مشخص و مستندسازی را برای برنامه های ADA اعمال کرد. طرح فعلی ANNA شامل حاشیه نویسی از تمام ساختارهای ADA به جز انجام وظایف است. پسوندهای مشابهی برای مشخصات رسمی را می توان به سایر زبان های شبیه به الگول مانند پاسکال، PL/1، پاسکال همزمان و مدولا ایجاد کرد. در اصل، این پسوندها زیرمجموعه های ANNA هستند. طراحی ANNA از ابتدا با چهار ملاحظات اصلی انجام شد: 1. ساخت حاشیه نویسی باید برای برنامه نویس ADA آسان باشد و تا حد امکان به نماد و مفاهیم ADA بستگی داشته باشد. 2. ANNA باید دارای ویژگی های زبانی باشد که به طور گسترده در مشخصات و مستندسازی برنامه ها استفاده می شود. 3. ANNA باید چارچوبی را فراهم کند که در آن تئوری های مختلف تثبیت شده برنامه های مشخص کننده رسمی در ADA اعمال شود. 4. حاشیه نویسی باید به همان اندازه برای کاربردهای مختلف ممکن در طول چرخه عمر یک برنامه مناسب باشد. چنین برنامه هایی نه تنها شامل آزمایش، اشکال زدایی و تأیید رسمی یک برنامه تمام شده، بلکه همچنین مشخص کردن بخش های برنامه در مراحل اولیه تجزیه و تحلیل نیازمندی ها و طراحی برنامه است.

This reference manual of ANNA is another volume addressed to the ADA community. ANNA is a language extension of ADA to include facilities for formally specifying the intended behavior of ADA programs. It is designed to meet a perceived need to augment ADA with precise machine-processable annotations so that well established formal methods of specification and documentation can be applied to ADA programs. The current ANNA design includes annotations of all ADA constructs except tasking. Similar extensions for formal specification can be made to other Algol-like languages such as Pascal, PL/1, Concurrent Pascal, and Modula; essentially, these extensions would be subsets of ANNA. The design of ANNA was undertaken from the beginning with four principal considerations: 1. Constructing annotations should be easy for the ADA programmer and should depend as much as possible on notation and concepts of ADA. 2. ANNA should possess language features that are widely used in the specification and documentation of programs. 3. ANNA should provide a framework within which the various established theories of formally specifying programs may be applied to ADA. 4. Annotations should be equally well suited for different possible applications during the life cycle of a program. Such applications include not only testing, debugging and formal verification of a finished program, but also specification of program parts during the earlier stages of requirements analysis and program design.