brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2025-10-10 06:51:13 +00:00
Code Issues Projects Releases Packages Activity

Medium syndication information

Browse source
This commit is contained in:
Brandon Rozek 2023-01-05 14:04:45 -05:00
parent e5a96d735a
commit c5ff5538a6
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
276 changed files with 371 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

1
content/blog/program-verification-hoare-logic-dafny.md
View file

@ -4,6 +4,7 @@ date: 2022-02-05T00:06:42-05:00
draft: false
tags: ["Formal Methods"]
math: false
medium_enabled: true
---
In the recitations that I'm giving for [Principles of Software](/ta/spring2022/csci2600/), we are going over reasoning through code using Hoare Logic and the program verifier Dafny. Microsoft Research designed Dafny to be similar to writing imperative code. The main difference is that you need to supply (pre/post)-conditions and the code to verify. Here's an example of how to reason about a simple statement by hand: