Interactive Theorem Provers: Ensuring Correctness in Programming
CS 472 – Provably Correct
Programming
William Mansky
1
Interactive Theorem Provers
•
In the theorem prover, we can:
1.
W
r
i
t
e
d
e
f
i
n
i
t
i
o
n
s
,
i
n
a
m
a
t
h
-
l
i
k
e
p
r
o
g
r
a
m
m
i
n
g
l
a
n
g
u
a
g
e
2.
W
r
i
t
e
p
r
o
o
f
s
a
b
o
u
t
t
h
o
s
e
d
e
f
i
n
i
t
i
o
n
s
,
u
s
i
n
g
l
o
g
i
c
“
t
a
c
t
i
c
s
”
3.
S
e
e
t
h
e
p
r
o
o
f
s
t
a
t
e
a
t
e
a
c
h
p
o
i
n
t
i
n
a
p
r
o
o
f
(
w
h
a
t
d
o
w
e
k
n
o
w
?
w
h
a
t
d
o
w
e
s
t
i
l
l
n
e
e
d
t
o
s
h
o
w
?
)
4.
A
u
t
o
m
a
t
i
c
a
l
l
y
c
h
e
c
k
t
h
a
t
e
a
c
h
s
t
e
p
o
f
o
u
r
p
r
o
o
f
s
i
s
v
a
l
i
d
2
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
3
4
Inductive Definitions
Inductive day :=
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.
5
day is a type
monday : day
tuesday : day
…
saturday : day
sunday : day
Types are sets!
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
7
How would you define the natural numbers?
8
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
9
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.
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
CS 472 Provably Correct Programming William Mansky
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
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
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
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
Inductive Definitions How would you define the natural numbers?
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
