From d30b852c5f04e32bfa73505215f9de3a31fc2b91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20L=C3=B6=C3=B6w?= Date: Wed, 18 Dec 2024 16:10:19 +0100 Subject: [PATCH] new name for the Gillian lab --- sphinx/wisl/index.rst | 2 +- sphinx/wisl/{lab.rst => verification-tutorial.rst} | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) rename sphinx/wisl/{lab.rst => verification-tutorial.rst} (94%) diff --git a/sphinx/wisl/index.rst b/sphinx/wisl/index.rst index c43af16b..e71ed342 100644 --- a/sphinx/wisl/index.rst +++ b/sphinx/wisl/index.rst @@ -6,4 +6,4 @@ WISL is an instantiation of Gillian to a simple while language with a C-style bl .. toctree:: :titlesonly: - lab + verification-tutorial diff --git a/sphinx/wisl/lab.rst b/sphinx/wisl/verification-tutorial.rst similarity index 94% rename from sphinx/wisl/lab.rst rename to sphinx/wisl/verification-tutorial.rst index fdec5047..d298bfb6 100644 --- a/sphinx/wisl/lab.rst +++ b/sphinx/wisl/verification-tutorial.rst @@ -1,7 +1,7 @@ -Initial Lab -=========== +Verification Tutorial +===================== -Welcome to the first Gillian lab! In this lab, you'll be using Gillian and its :doc:`debugger ` to add missing proof tactics to while programs and verify them with :doc:`/wisl/index`. +Welcome to this verification tutorial lab! In this lab, you'll be using Gillian and its :doc:`debugger ` to add missing proof tactics to while programs and verify them with :doc:`/wisl/index`. You are provided with 2 files: ``sll.wisl`` and ``dll.wisl``, which contain predicates, lemmas and functions. The goal is to use WISL and its debugger to insert the right proof tactics for every function to successfully verify. Note that in practice, Gillian can infer a lot of these annotations on its own; for this lab, we disable this by using Gillian's "manual" mode.