Я читаю руководство по языку VDM++. Мой вопрос в том, что в некоторых случаях он использует ";" в конце утверждения и где-то в том же утверждении он не использует «;».
Ниже приведен пример
public Top : () ==> Elem
Top() ==
return (hd stack);
if test
then OpCall()
else return FunCall()
Точки с запятой являются разделителями в VDM, а не терминаторами, как в Java и C. Таким образом, вам нужна точка с запятой, когда две вещи идут последовательно, например, два определения или два утверждения. Но вам не нужен разделитель, если в «блоке» есть только одна вещь.
Таким образом, вашему первому примеру может понадобиться точка с запятой в конце, если следует другое определение, но не в том случае, если "Top" является последним определением в классе/модуле.
В вашем втором примере точка с запятой после OpCall() не нужна, потому что это один оператор в предложении «тогда». Вам может понадобиться точка с запятой после FunCall(), если за этим if/then/else следует другой оператор, но не иначе.
Сказав это, синтаксический анализатор VDMJ прощает и допускает ложные точки с запятой в некоторых местах, даже если они строго не требуются.
