最短路径问题
采用Dijkstra算法计算一个节点到其他所有节点的最短路径。 （验证时间约 133sec）
[Back to Index]
验证特点：引理和用于证明引理的引理，量化断言，逻辑函数，归纳谓词，幽灵语句
标注说明：函数前条件：给出最短距离数组的性质；
函数后条件：所有节点的最短路径都已计算过，并且0到其他N-1个节点的路径为最短路径。
程序样例 
采用Dijkstra算法计算一个节点到其他所有节点的最短路径。 （验证时间约 133sec）
验证特点：引理和用于证明引理的引理，量化断言，逻辑函数，归纳谓词，幽灵语句
标注说明：函数前条件：给出最短距离数组的性质；
函数后条件：所有节点的最短路径都已计算过，并且0到其他N-1个节点的路径为最短路径。
程序样例