Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

07.06.2016 | Ausgabe 2/2017

Journal of Automated Reasoning 2/2017

Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 2/2017
Autoren:
Ana Cristina Rocha-Oliveira, André Luiz Galdino, Mauricio Ayala-Rincón
Wichtige Hinweise
Work supported by CNPq Universal Grant 476952/2013-1.

Abstract

Orthogonality is a discipline of programming which syntactically guarantees determinism of functional specifications. Essentially, orthogonality avoids critical forks in term rewriting systems (TRSs) twofold: avoiding overlappings between left-hand sides of the rules (non-ambiguity) prohibiting rules in the definitions of functions that may apply simultaneously and forbidding repetitions of variables in the left-hand side of the rules (left-linearity) that may produce forks. In the theory of term rewriting systems, determinism is captured by the well-known property of confluence that is a consequence of orthogonality. This work describes a complete formalization in PVS of the theorem of confluence of orthogonal term rewriting systems. The formalization includes definitions and results on parallel reduction, in particular Rosen’s Parallel Moves Lemma. It is made available as a PVS theory orthogonality inside the directory TRS of the NASA Langley PVS Library. Like all of TRS, orthogonality is intended to stay close to textbook proofs. The present proof uses the Parallel Moves Lemma at dominating positions of a parallel context. In this manner, all parallel forks filling the holes of the context are joined and, as result, a term of joinability for the whole fork is constructed.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit dem Kombi-Abo erhalten Sie vollen Zugriff auf über 1,8 Mio. Dokumente aus mehr als 61.000 Fachbüchern und rund 500 Fachzeitschriften aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit dem Wirtschafts-Abo erhalten Sie Zugriff auf über 1 Mio. Dokumente aus mehr als 45.000 Fachbüchern und 300 Fachzeitschriften aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit dem Technik-Abo erhalten Sie Zugriff auf über 1 Mio. Dokumente aus mehr als 40.000 Fachbüchern und 300 Fachzeitschriften aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Premium Partner

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung

Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier  - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis.
Jetzt gratis downloaden!

Bildnachweise