## Stream: Coq users

### Topic: floyd-warshall algorithm

#### 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

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: Jan 28 2023 at 05:02 UTC