Jacob (Mar 29 2021 at 21:17): Jacob (Mar 29 2021 at 21:17):I am trying to use cop to prove floyd-warshall algorithm. This is the
Jacob (Mar 29 2021 at 21:17):1 let dist be a |V| × |V| array of minimum distances initialized to ∞ (infinity)
2 for each vertex v
3 dist[v][v] ← 0
4 for each edge (u,v)
5 dist[u][v] ← w(u,v) // the weight of the edge (u,v)
6 for k from 1 to |V|
7 for i from 1 to |V|
8 for j from 1 to |V|
9 if dist[i][j] > dist[i][k] + dist[k][j]
10 dist[i][j] ← dist[i][k] + dist[k][j]
11 end if
Jacob (Mar 29 2021 at 21:18):pseudocode
Jacob (Mar 29 2021 at 21:19):I am not sure what should I do first
Jacob (Mar 29 2021 at 21:45):Does anyone know how to do this?
Ignat Insarov (Mar 30 2021 at 05:48):I think the first step would be to write this algorithm up in the Gallina language and have Coq automatically check that it is always terminating.
Yannick Forster (Mar 30 2021 at 08:47):I think it would help if you provide some context :) Here are some interesting questions which make it easier to help: Do you want to obtain a verified implementation (e.g. by extraction to OCaml)? Or are you only interested in verifying the algorithm mathematically? Did you pick the exercise yourself, or is it part of a course / book? How much experience with Coq do you already have?
Last updated: Oct 13 2024 at 01:02 UTC