Floyd-Warshall algorithm: Difference between revisions
Content added Content deleted
| Line 378: | Line 378: | ||
This implementation uses non-linear types that will leak memory. However, such memory leaks are what Boehm GC is made to deal with. (Also, such leaks are inconsequential in a program like this one.) |
This implementation uses non-linear types that will leak memory. However, such memory leaks are what Boehm GC is made to deal with. (Also, such leaks are inconsequential in a program like this one.) |
||
Removing one of the runtime assertions ('''assertloc''') might prevent compilation. This is a difference between ATS and most other languages. For the template functions '''square_array_get_at''' and '''square_array_set_at''', there is a '''praxi''' (an axiom) instead of assertions, and so there is no runtime penalty. A proof of the "axiom" could have been derived from the properties of multiplication, in case I had any doubts (and one may be surprised how often one is wrong about a lemma), but I simply declared it as an axiom. |
Removing one of the runtime assertions ('''assertloc''') might prevent compilation. This is a difference between ATS and most other languages. For the template functions '''square_array_get_at''' and '''square_array_set_at''', there is a '''praxi''' (an axiom) instead of assertions, and so, by contrast, there is no runtime penalty. A proof of the "axiom" could have been derived from the properties of multiplication, in case I had any doubts (and one may be surprised how often one is wrong about a lemma), but I simply declared it as an axiom. |
||