VDMのfunctionとoperation

VDMでは、functionとoperationの使い分けって微妙です。
これ、Javaではどちらもメソッドにあたります。
どう使い分けするのかが悩みます。
しかも、文法が結構違うので、途中で簡単に変更できないのも厄介です。
そのため、最初にどちらで記述すべきかを決めてるのが重要です。
operationかfunctionで記述するか、を決めるのは慎重にすべきです。