如何推导给定Hoare三元组对应代码的循环不变式？

各位大佬好，我最近在学习Hoare逻辑里的循环不变式，遇到了一个搞不懂的问题，想请大家帮忙指导下：

问题背景 #

我需要从以下代码对应的Hoare三元组中推导或选择循环不变式，相关内容如下：

对应的Hoare三元组 #

(|true|) x = 0 ; s = 0 ; while ( x ≤ n ) { s = s + x ; x = x + 1 ; } (|s = n(n + 1)/2|)

代码逻辑 #

这段代码的功能是通过循环累加计算从0到n的整数和，最终要满足后置条件 s = n(n + 1)/2。

我的困惑 #

目前已知给出的循环不变式解是 s = (x-1)*x/2 ∧ (x ≤ n +1)，但我完全理解不了这个解的推导过程。希望有人能帮我讲解这个解是怎么来的，或者教教我怎么从这段代码里推导得出其他有效的循环不变式。

内容的提问来源于stack exchange，提问作者user6797155