This function allows you to sum sets of integers in Rodin.
It is based on verified recursive sum algorithm and proven automatically in Rodin with ProB.
This can also be used as an inspiration to do some more advanced things with Event-B Rodin.
Simply imports the files from /sumFunction into your project and add sum_ctx to the clause SEES of the machine in which you need it.
You can then use the function as any other function: sum(S)
For animations, you can mute the first line sum : POW(INT) --> INT & into the comment if you don't want to see an error.
sum -- sum -- Sum of elements of set \
| Description | sum(S) is an expression that gives the sum of each element in the given set. it is only defined for finite sets. |
| Definition | sum(S) = s_1 + s_2 + ... + s_n where s_n are integers elements of S. |
| Types | sum(S) is an integer (:INT -or Z-) with S being a POW(Z) (powerset of integers) |
| WD | ? |
Made with Rodin Platform Version: 3.4.0-6980ca1 on Windows 10 amd64.
Any contribution is welcome !