دورية أكاديمية
An Approach to Automated Reasoning About Operational Semantics.
| العنوان: | An Approach to Automated Reasoning About Operational Semantics. |
|---|---|
| المؤلفون: | Cant, A., Ozols, M. A. |
| المساهمون: | DEFENCE SCIENCE AND TECHNOLOGY ORGANIZATION CANBERRA (AUSTRALIA) |
| المصدر: | DTIC AND NTIS |
| سنة النشر: | 1994 |
| المجموعة: | Defense Technical Information Center: DTIC Technical Reports database |
| مصطلحات موضوعية: | Computer Programming and Software, PROGRAMMING LANGUAGES, COMPUTER PROGRAM VERIFICATION, SOFTWARE ENGINEERING, REQUIREMENTS, AUTOMATION, DATA PROCESSING SECURITY, COMPARISON, REASONING, COMPUTER LOGIC, SEMANTICS, OPERATING SYSTEMS(COMPUTERS), AUSTRALIA, CONTROL SEQUENCES, FOREIGN REPORTS |
| الوصف: | The assurance of the safety or security of critical software rests on a clear understanding of the formal semantics of the programming language used. Operational semantics is the most widely used means of formally defining a language. The need for high levels of assurance, along with the complexity of these definitions for real programming languages, means that tool support is essential for carrying out reasoning about code with respect to the language definition. In this paper, we describe a generic approach to automated reasoning about the operational semantics of programming languages. As an application of this approach, we describe the construction of an environment for reasoning about programs written in a functional subset of ML. The system we describe (called Elle) captures the formal operational semantics definition of a large subset of Standard ML within the theorem prover Isabelle, and provides some support for the verification of ML programs. (AN) |
| نوع الوثيقة: | text |
| وصف الملف: | text/html |
| اللغة: | English |
| العلاقة: | http://www.dtic.mil/docs/citations/ADA291127Test |
| الإتاحة: | http://www.dtic.mil/docs/citations/ADA291127Test http://oai.dtic.mil/oai/oai?&verb=getRecord&metadataPrefix=html&identifier=ADA291127Test |
| حقوق: | APPROVED FOR PUBLIC RELEASE |
| رقم الانضمام: | edsbas.BD598A5A |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |