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

Removing URL prefix for local URLs in blog posts

Browse source
This commit is contained in:
Brandon Rozek 2022-12-18 12:25:45 -05:00
parent b02794d677
commit 6dc8bfbb89
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
21 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -6,7 +6,7 @@ tags: ["Formal Methods"]
math: false
---
In the recitations that I'm giving for [Principles of Software](https://brandonrozek.com/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:
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:
```csharp
// Precondition: x > 0