We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport's definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.

翻译：我们提出一个分布式程序规约的格结构，其序关系表示可实现性/精化。规约通过相对执行迹的子集族建模——这些迹编码了状态转换的局部序关系，而非根据全局时钟的绝对时间顺序。这是为了克服同步过程中基本的物理困难。该规约格结构通过若干成熟的数学工具构建并分析：单纯集非退化胞腔集用于建模相对迹、预层用于通过变量拓扑空间参数化这些迹、信息代数揭示了程序正确性上的新颖约束条件。后者将程序规约工作纳入Abramsky等人提出的不断扩展的语境语义学框架中。在此程序规约模型下，语境性表现为一致性准则的失效——该准则可与Lamport对顺序一致性的定义相类比。信息代数理论还提出了用于验证该准则的高效局部计算算法。本文中的创新构造已在证明辅助工具Isabelle/HOL中得到验证。