Published September 19, 2022 | Version v1
Publication Open

Indexed and fibered structures for partial and total correctness assertions

Creators

  • 1. University of Bergen
  • 2. Pontifical Catholic University of Rio de Janeiro

Description

Abstract Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented, and concurrent programs. Here we focus on partial and total correctness assertions within the framework of Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed and fibered category theory. We consider Hoare formulas with local, finite contexts, of program and logical variables. The structural features of Hoare assertions are presented in an indexed setting, while the logical features of deduction are modeled in the fibered one.

⚠️ This is an automatic machine translation with an accuracy of 90-95%

Translated Description (Arabic)

يتمتع منطق هور التجريدي بتقليد طويل في التحقق الرسمي وقد تم تطويره واستخدامه باستمرار للتحقق من فئة واسعة من البرامج، بما في ذلك البرامج المتسلسلة والموجهة للكائنات والمتزامنة. نركز هنا على تأكيدات الصحة الجزئية والكاملة في إطار منطق هور ونوضح أن التحليل الفئوي الشامل لدلالاته البديهية يحتاج إلى لغات نظرية الفئة المفهرسة والألياف. نعتبر صيغ هور مع السياقات المحلية والمحدودة للبرنامج والمتغيرات المنطقية. يتم تقديم السمات الهيكلية لتأكيدات هور في إطار مفهرس، في حين يتم نمذجة السمات المنطقية للخصم في الإطار الليفي.

Translated Description (French)

Abstract Hoare Logic a une longue tradition de vérification formelle et a été continuellement développé et utilisé pour vérifier une large classe de programmes, y compris les programmes séquentiels, orientés objet et simultanés. Nous nous concentrons ici sur les assertions de correction partielle et totale dans le cadre de la logique de Hoare et montrons qu'une analyse catégorique complète de sa sémantique axiomatique nécessite les langages de la théorie des catégories indexée et fibrée. Nous considérons les formules Hoare avec des contextes locaux, finis, de variables de programme et logiques. Les caractéristiques structurelles des assertions Hoare sont présentées dans un cadre indexé, tandis que les caractéristiques logiques de la déduction sont modélisées dans le cadre fibré.

Translated Description (Spanish)

La lógica abstracta de Hoare tiene una larga tradición en la verificación formal y se ha desarrollado y utilizado continuamente para verificar una amplia clase de programas, incluidos los programas secuenciales, orientados a objetos y concurrentes. Aquí nos centramos en las afirmaciones de corrección parcial y total dentro del marco de la lógica de Hoare y mostramos que un análisis categórico exhaustivo de su semántica axiomática necesita los lenguajes de la teoría de categorías indexadas y fibrosas. Consideramos fórmulas de Hoare con contextos locales, finitos, de programa y variables lógicas. Las características estructurales de las afirmaciones de Hoare se presentan en un entorno indexado, mientras que las características lógicas de la deducción se modelan en el de fibra.

Files

div-class-title-indexed-and-fibered-structures-for-partial-and-total-correctness-assertions-div.pdf.pdf

Files (694.5 kB)

⚠️ Please wait a few minutes before your translated files are ready ⚠️ Note: Some files might be protected thus translations might not work.
Name Size Download all
md5:d9fd7c0194b49f0bc78528265f931cb1
694.5 kB
Preview Download

Additional details

Additional titles

Translated title (Arabic)
الهياكل المفهرسة والألياف لتأكيدات الصحة الجزئية والكاملة
Translated title (French)
Structures indexées et fibrées pour les assertions d'exactitude partielle et totale
Translated title (Spanish)
Estructuras indexadas y fibrosas para afirmaciones de corrección parcial y total

Identifiers

Other
https://openalex.org/W4296364777
DOI
10.1017/s0960129522000275

Is supplement to
https://openalex.org/W4297797338 (Other)
https://openalex.org/W3210461265 (Other)
https://openalex.org/W2401536999 (Other)
https://openalex.org/W2347161843 (Other)
https://openalex.org/W2256268268 (Other)
https://openalex.org/W2226137800 (Other)
https://openalex.org/W2129865151 (Other)
https://openalex.org/W2117210984 (Other)
https://openalex.org/W2095484401 (Other)
https://openalex.org/W2038289817 (Other)

GreSIS Basics Section

Is Global South Knowledge
Yes
Country
Brazil

References

  • https://openalex.org/W1536810838
  • https://openalex.org/W1966305152
  • https://openalex.org/W1982145886
  • https://openalex.org/W1984184513
  • https://openalex.org/W2010883554
  • https://openalex.org/W2066210260
  • https://openalex.org/W2075350371
  • https://openalex.org/W2079393871
  • https://openalex.org/W2117557111
  • https://openalex.org/W2130427425
  • https://openalex.org/W30041542
  • https://openalex.org/W3013738153
  • https://openalex.org/W3036611088
  • https://openalex.org/W3094043897
  • https://openalex.org/W3145817034
  • https://openalex.org/W4249188466
  • https://openalex.org/W4251228600
  • https://openalex.org/W4254994720
  • https://openalex.org/W4296415990
  • https://openalex.org/W4388310185
  • https://openalex.org/W564762911