我是一位对信息检索感兴趣的软件开发人员。目前，我正在从事我的第三个搜索引擎项目，对于一次又一次地编写具有相同错误等的样板代码感到非常沮丧。
基本搜索引擎是一种非常简单的野兽，可以用由两个“层”组成的正式语言来描述：
“原始层”（或公理，内核语言-不知道如何命名）。它们由多个集合（作为一组资源-文件，网站），集合上的关系（作为“站点A到站点B的链接”）以及简单的操作（例如“向资源A开放流”，“从流中读取记录”， “合并N个流”，“按字段F对记录的索引集”等。此外，还有很多数据转换，例如“以YAML格式保存流”，“从XML格式加载流”等。
“应用层”-形成搜索引擎生命周期的几个非常高级的操作，例如“收获新资源”，“抓取资源”，“将抓取的资源合并到数据库”，“索引抓取的资源”，“合并索引”等等。每一项高级操作都可以用从1开始的“原始语”来表达。
这样的高级表示可以很容易地测试，甚至可以被正式证明，并可以以所选的编程语言来实现（或代码生成）。
那么，问题是：有人以严格的自上而下的方式正式地，严格地（甚至在代数/群论的层面）设计系统吗？我可以阅读以了解什么？
最佳答案
关键系统（核电站，飞机，火车控制系统等）的开发方法与您所寻找的类似，是自上而下的。但是高层甚至根本不是编程的。这与内核层和应用程序层无关，而是与精炼成组件，子组件的高层设计有关，每个级别都有精确的规范。
规范可以是正式的（打算在指定组件可用后自动进行验证），也可以不是正式的（旨在通过测试，代码审查或任何适当的方法进行验证）。坦率地说，在2009年，大多数情况下它们并不是正式的，尽管趋势显然是朝着这个方向发展。
由于您在问题的标签中提到了正式的方法，因此您必须对该主题感兴趣，但是目前这是一个利基市场。我尤其看不到如何将这些方法经济地应用于搜索引擎项目。无论如何，如果您想了解有关这些方法如何在其工作领域中应用的更多信息，请参见以下几个链接：
有人提到Z：Z是规范语言，您在其中完善和精炼规范直到成为可执行文件的框架称为B。您可能也对Alloy感兴趣。最后，对于现有的编程语言，存在正式的规范语言。这种趋势始于Java的JML，并启发了其他许多人。我在一群为C ACSL定义了这种规范语言的人中工作。