Academic Journal
A Machine Verified Distributed Sorting Algorithm
| العنوان: | A Machine Verified Distributed Sorting Algorithm |
|---|---|
| المؤلفون: | Jørgen Andersen, Ed Harcourt, K. V. S. Prasad |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.brics.dk/RS/96/Ref/BRICS-RS-96-Ref/././././RS/96/4/BRICS-RS-96-4.ps.gz. |
| سنة النشر: | 1996 |
| المجموعة: | CiteSeerX |
| الوصف: | We present a verification of a distributed sorting algorithm in ALF, an implementation of Martin Löf's type theory. The implementation is expressed as a program in a priortized version of CBS, (the Calculus of Broadcasting Systems) which we have implemented in ALF. The specification is expressed in terms of an ALF type which represents the set of all sorted lists and an HML (Hennesey-Milner Logic) formula which expresses that the sorting program will input any number of data until it hears a value triggering the program to begin outputting the data in a sorted fashion. We gain expressive power from the type theory by inheriting the language of data, state expressions, and propositions. |
| نوع الوثيقة: | text |
| وصف الملف: | application/postscript |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.6485; http://www.brics.dk/RS/96/Ref/BRICS-RS-96-Ref/././././RS/96/4/BRICS-RS-96-4.ps.gz |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.6485 http://www.brics.dk/RS/96/Ref/BRICS-RS-96-Ref/././././RS/96/4/BRICS-RS-96-4.ps.gz |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.C470B2DE |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |