| If your algorithm does not at all depend on the result of division, you can replace it by a constant parameter Div(_,_). For theorem proving, you should then be able to prove the properties that you are interested in. For model checking, you will still need to provide an instance of that operator, say Div(x,y) == 42 but you can run TLC with different definitions to become confident that the definition is indeed irrelevant. However, if this is true, it sounds like you could write an even more abstract specification, such as getting rid of variables to which division is applied. If your algorithm depends on certain properties of division but not the precise result you can state those in an ASSUME clause, say, ASSUME \A x,y \in Int : y # 0 => Div(x,y) \in Int /\ Div(x,y) < x Stephan
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/862EFD8E-1E6D-43B4-92CD-A707E1081FB1%40gmail.com. |