6260 Notes: Happy Dafny

6260 notes: 义务即命题,归纳抄函数,六句总结

16 minute read Published: 2026-08-29

6260 notes: termination1——decreases、模子与两次读数

19 minute read Published: 2026-08-29

6260 notes: chunks,引理辅助终止

2 minute read Published: 2026-08-28

6260 notes: wfSet,良构不变量,引理调引理

3 minute read Published: 2026-08-27

6260 notes: shadowing、ghost、集合引理、take/drop

12 minute read Published: 2026-08-19