在哪里可以找到使用Hoare逻辑验证Isabelle/HOL程序中程序的更复杂的示例？
我最近了解到在Isabelle/HOL中使用Hoare逻辑进行程序验证的这一方面。我发现本教程中的示例 是简单的例子 (http://www.inf.ed.ac.uk/teaching/courses/ar/HoareLogicLecture.thy(。 在哪里可以找到使用Hoare逻辑验证Isabelle/HOL程序中程序的更复杂的示例？
seL4 证明可能符合要求。例如，跨内核功能规范的不变保持证明：https://github.com/NICTA/l4v/blob/master/proof/invariant-abstract/README.md
javascript python java c# php android html jquery c++ css ios sql mysql arrays asp.net json python-3.x ruby-on-rails .net sql-server django objective-c excel regex ruby linux ajax iphone xml vba spring asp.net-mvc database wordpress string postgresql wpf windows xcode bash git oracle list vb.net multithreading eclipse algorithm macos powershell visual-studio image forms numpy scala function api selenium