Interactive Theorem Provers: Ensuring Correctness in Programming

Slide Note
Embed
Share

Explore the world of Interactive Theorem Provers, where you can write definitions, proofs, and automatically validate the correctness of your code. Learn about writing definitions in Coq, inductive definitions, and completing exercises to solidify your understanding.


Uploaded on Oct 07, 2024 | 0 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

E N D

Presentation Transcript


  1. CS 472 Provably Correct Programming William Mansky

  2. Interactive Theorem Provers In the theorem prover, we can: 1. Write definitions definitions, in a math-like programming language 2. Write proofs proofs about those definitions, using logic tactics 3. See the proof state proof state at each point in a proof (what do we know? what do we still need to show?) 4. Automatically check check that each step of our proofs is valid

  3. Writing Definitions in Coq The definition language of Coq is an OCaml-like functional programming language, called Gallina Key features: inductive types, pattern matching, and recursion Purpose is to define mathematical objects, not to write programs (though the two are often the same!) See Basics.v from the textbook

  4. Inductive Definitions Types are sets! Inductive day := | monday | tuesday | wednesday | thursday | friday | saturday | sunday. monday,tuesday, ,saturday,sunday day is a set monday day tuesday day saturday day sunday day day is a type monday : day tuesday : day saturday : day sunday : day

  5. Exercise: nandb Complete the exercise nandb in Basics.v: fill in the definition of nandb, and prove that the examples work Submit your definition and example proofs for Exercise 1/10 on Gradescope It may help to refer to the definitions of negb, andb, and orb earlier in the file

  6. Inductive Definitions How would you define the natural numbers?

  7. HW1: Basics.v Complete all the exercises in Basics.v (you may skip the one marked optional) You can run BasicsTest.v to make sure you ve gotten all of them; there s also an autograder on Gradescope, though it checks more problems than were assigned Due Sunday 1/21 at 11:59 PM Submit via Gradescope

Related


More Related Content