Verifizierte Datentypen für Solidity

Typ:	MA / PdF
Datum:
Betreuer:	Jonas Schiffl
Aushang:

Motivation und Aufgabenstellung

Solidity ist eine Programmiersprache, mit der Smart Contracts für die Ethereum-Plattform geschrieben werden. Weil Smart Contracts viel Geld verwalten und Fehler schwer zu beheben sind, ist es wichtig, dass der Quellcode schon bei Auslieferung korrekt ist.

In Solidity sind diverse nützliche Datenstruturen nicht nativ vorhanden, wären aber für bestimmte Anwendungsfälle sinnvoll. Für diese Datenstrukturen sollen Referenzimplementierungen gegeben werden, evtl mit formaler Spezifikation und Korrektheitsbeweisen. Entwickler müssen diese Datentypen nun nicht mehr selbst implementieren, sondern können auf bestehende, vertrauenswürdige Implementierungen zurückgreifen.

Beispiele für solche Datenstrukturen sind

• Listen
• Iterable Mappings
• Caller-specific Mappings (i.e. mappings, die vom Aufrufer nur an einer einzigen Stelle, z.B. seiner eigenen Adresse, modifiziert werden können)
• Baumdatenstrukturen
• Polymorphismus

Anforderungen

Die Inhalte der Vorlesung "Formale Systeme" (oder vergleichbar) sollten bekannt sein. Programmiererfahrung sowie die Bereitschaft, eine neue Programmierumgebung kennenzulernen, sind von Vorteil.