Die Korrektheit von Software ist ein zentrales Ziel der Softwareentwicklung. Eine Mög- lichkeit die Korrektheit zu verbessern, ist das Verwenden starker und deskriptiver Typen, die Korrektheitseigenschaften als Typen kodieren, und die Kompatibilität mit dem Pro- gramm mit Hilfe von Typsystemen verifizieren. Insbesondere Refinement Types haben gezeigt, dass selbst mit einem Verifikationssystem, das auf eine entscheidbare Logik be- schränkt ist, komplizierte Eigenschaften leicht ausgedrückt und automatisch verifiziert werden können.

Bestehende Ansätze zur Anpassung von Refinement Types von funktionalen an impe- rative Sprachen haben jedoch gezeigt, dass die Existenz von veränderbaren Daten und Referenzen Kompromisse bei mindestens einer der Kerneigenschaften von Refinement Types mit sich bringt, nämlich der automatisierten, entscheidbaren Verifikation und ei- ner minimalen, leicht verständlichen Spezifikation.

Aufgabe:

In dieser Arbeit soll ein Refinement-Type-System für eine sinnvolle Untermenge von Rust erarbeitet werden, das Rusts Beschränkung auf unique mutable Referenzen ausnutzt.

Schlüsselworte

Rust, Refinement Types 

Veröffentlichungen

Veröffentlichung

LiquidRust: Refinement Types for Imperative Languages with Ownership

Betreuer

Wissenschaftliche Mitarbeiter
Sebastian Graf

Studenten

Ehemalige Studenten
Carsten Csiky