We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nondeterministic branching and (2) weighting execution traces. Weights can be numbers but also other objects like words from an alphabet, polynomials, formal power series, or cardinal numbers. We argue that weighted programming as a paradigm can be used to specify mathematical models beyond probability distributions (as is done in probabilistic programming). We develop weakest-precondition- and weakest-liberal-precondition-style calculi \`{a} la Dijkstra for reasoning about mathematical models specified by weighted programs. We present several case studies. For instance, we use weighted programming to model the ski rental problem - an optimization problem. We model not only the optimization problem itself, but also the best deterministic online algorithm for solving this problem as weighted programs. By means of weakest-precondition-style reasoning, we can determine the competitive ratio of the online algorithm on source code level.

翻译：更具体地说,我们所调查的加权程序就像通常的必备程序,具有两个额外特征:(1)非决定性分支和(2)加权执行痕迹。加权可以是数字,也可以是字母、多面体、正式权力序列或主号等字词。我们主张,加权程序可以用来指定概率分布以外的数学模型(如概率编程中所做的那样 ) 。我们开发了最弱和最弱的自由主义预设模式(calculi ⁇ a) la Dijkstra, 用于对加权程序指定的数学模型进行推理。我们介绍了几个案例研究。例如,我们使用加权程序模拟滑雪租赁问题――优化问题。我们不仅模拟优化问题本身,而且模拟作为加权程序解决该问题的最佳确定性在线算法。通过最弱的假设推理,我们可以确定源码级别的在线算法的竞争性比率。