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中完成验证。