Amazon veröffentlicht Dafny-basierten Programmierüberprüfungskurs

Amazon hat Lehrmaterialien zur Programmverifikation mit Dafny veröffentlicht. Der Kurs geht über die grundlegende Dafny-Programmierung hinaus und untersucht seine Fähigkeiten als Proof-Assistant. Er ist in drei Teile gegliedert: Teil 1 stellt die Programmiersprache Dafny vor; Teil 2 untersucht Dafny als Proof-Assistant und behandelt formale Beweismethoden wie die natürliche Deduktion; und Teil 3 wendet dieses Wissen auf die Programmverifikation an und behandelt funktionale, imperative und objektorientierte Programme. Diese Ressource eignet sich sowohl für Anfänger als auch für erfahrene Dafny-Entwickler und bietet einen umfassenden Ansatz zur Programmverifikation.