Stream: Coq users

Topic: floyd-warshall algorithm


view this post on Zulip Jacob (Mar 29 2021 at 21:17):

I am trying to use cop to prove floyd-warshall algorithm. This is the

view this post on Zulip 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

view this post on Zulip Jacob (Mar 29 2021 at 21:18):

pseudocode

view this post on Zulip Jacob (Mar 29 2021 at 21:19):

I am not sure what should I do first

view this post on Zulip Jacob (Mar 29 2021 at 21:45):

Does anyone know how to do this?

view this post on Zulip 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.

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC