Vorlesungen

Unter https://github.com/HS-Flensburg-LBS/Language-based-Security finden Sie die Coq-Skripte, die wir in der Vorlesung zusammen entwickelt haben. In der Vorlesung werden Kapitel des Buchs Software Foundations - Volume 1 besprochen. Hier wird aufgelistet, welche Kapitel jeweils besprochen wurden.

1. Vorlesung

Inhalte der Abschnitte Preface und Data and Functions

2. Vorlesung

Inhalte der Abschnitte Proof by Simplification, Proof by Rewriting, Proof by Case Analysis und Unfolding Definitions

3. Vorlesung

Inhalte der Abschnitte Proof by Induction, Lists of Numbers und Reasoning About Lists

4. Vorlesung

Inhalte der Abschnitte Polymorphism, Functions as Data, The apply Tactic und The apply with Tactic

5. Vorlesung

Inhalte der Unterabschnitte Conjunction, Disjunction und Falsehood and Negation des Abschnitts Logical Connectives

6. Vorlesung

Inhalte der Unterabschnitte Logical Equivalence und Existential Quantification des Abschnitts Logical Connectives und des Abschnitts Programming with Propositions

7. Vorlesung

Inhalte der Abschnitte Propositions vs. Booleans und Working with Decidable Properties

8. Vorlesung

Inhalte des Abschnitts Inductively Defined Propositions

9. Vorlesung

Inhalte des Abschnitts Kryptoschemata

Verwendung von Coq

In diesem Abschnitt werden technische Aspekte bei der Verwendung von Coq erklärt.

Übersetzung eines Projektes

Ab der dritten Aufgabe besteht das Coq-Projekt aus mehreren Coq-Dateien. Um eine Coq-Datei in einer anderen Coq-Datei importieren zu können, müssen die Dateien zuerst übersetzt werden. Coq verwendet hierfür ein Makefile. Mit dem folgenden Kommando kann dieses Makefile erstellt werden.

coq_makefile -f _CoqProject *.v -o Makefile

Mit dem folgenden Kommando wird das Makefile ausgeführt und die Coq-Dateien im Verzeichnis übersetzt.

make

Unter MacOS und Linux steht das make-Kommando standardmäßig zur Verfügung. Unter Windows muss das Kommando erst einmal installiert werden. Der folgende Abschnitt gibt Hinweise, wie make unter Windows installiert werden kann.

Installation von make unter Windows

Wenn ihr unter Windows arbeitet, muss make zuerst installiert werden. Dafür gibt es recht viele verschiedene Optionen. Hier wird eine mögliche Option illustriert.

  • Laden Sie die Datei make-4.4.1-without-guile-w32-bin.zip von der Seite https://sourceforge.net/projects/ezwinports/files/ herunter.
  • Erstellen Sie im Ordner C:\Benutzer\NUTZERNAME einen Ordner bin (NUTZERNAME dabei durch den eigenen Nutzernamen ersetzen).
  • Entpacken Sie das Zip, indem Sie die Datei make-4.4.1-without-guile-w32-bin.zip im Windows Explorer öffnen.
  • Kopieren Sie die Datei make.exe aus der entpackten ZIP-Datei in den Ordner C:\Benutzer\NUTZERNAME\bin.
  • Fügen Sie Coq zum Windows-Pfad hinzu:
    • Suchen Sie in der Windows-Suche “Umgebungsvariablen für dieses Konto bearbeiten”.
    • Wählen Sie die unter den Benutzervariablen die Variable mit dem Namen Path.
    • Drücken Sie Bearbeiten... und fügen Sie das Verzeichnis, in dem Coq installiert ist, hinzu, zum Beispiel C:\Coq-Platform~8.16~2022.09\bin.

Um make jetzt zu nutzen, erstellen Sie eine neue Git-Bash im Aufgabenordner. In der Git-Bash sollten jetzt die Befehle coq_makefile und make funktionieren.