jennalwise / graphblas-verif

Formal verification of the GraphBLAS C API implementation by Tim Davis using Frama-C/WP.
Other
5 stars 1 forks source link

A valid semiring should have a valid commutative monoid #6

Open jennalwise opened 6 years ago

jennalwise commented 6 years ago

Should check that the valid monoid within a semiring is in fact commutative. Monoid validity should check for algebraic properties of monoid structures, such as having an associative binary operator and a proper identity for that operator. Therefore, resolution of this issue depends on resolution of issue 2.

jennalwise commented 6 years ago

This extends to other operations using semirings: