VDM++とJavaのコンストラクタ

VDM++はオブジェクト指向で、Javaを参考にした面もあって、似ている部分がたくさんある。今回は、VDM++とJavaで色々並べて書いてみようと思う。ちょっと長いです。

デフォルトコンストラクタと引数ありコンストラクタ

VDM++

class Super
  operations
    public Super : () ==> Super
    Super() == def - = new IO().echo("Super class constructor called.¥n") in skip;
end Super

class Child is subclass of Super
  operations
    public Child : () ==> Child
    Child() == def - = new IO().echo("Child class constructor called.¥n") in skip;
    
    public Child : seq of char ==> Child
    Child(s) == def - = new IO().echo(s ^ "¥n") in skip;
end Child

Java

これをJavaで書くとこうなる。VDM++との違いは、記法の違いぐらいしかない。
※ 実行できるように、mainメソッドを追加してます

public class Super {
  public Super() {
    System.out.println("Super class constructor called.");
  }
}

public class Child extends Super {
  public Child() {
    System.out.println("Child class constructor called.");
  }

  public Child(String s) {
    System.out.println(s);
  }
  
  public static void main(String[] args) {
    new Child();
    new Child("aaa");
  }
}

実行してみても、まったく同じ。

VDM++

インタープリタでコマンドを入力
>> init
>> print new Child()

Super class constructor called.
Child class constructor called.

>> print new Child("aaa")

Super class constructor called.
aaa

Java

Super class constructor called.
Child class constructor called.

Super class constructor called.
aaa

デフォルトコンストラクタなしで引数ありコンストラクタあり

違いが出るのは、こんなコードを書いた時。

VDM++

class Super
  operations
    public Super : () ==> Super
    Super() == def - = new IO().echo("Super class constructor called.¥n") in skip;
end Super

class Child is subclass of Super
  operations
    public Child : seq of char ==> Child
    Child(s) == def - = new IO().echo(s ^ "¥n") in skip;
end Child

Java

public class Super {
  public Super() {
    System.out.println("Super class constructor called.");
  }
}

public class Child extends Super {
  public Child(String s) {
    System.out.println(s);
  }
  
  public static void main(String[] args) {
    new Child();
  }
}

VDM++

これをVDM++は実行するとこうなる。

>> init
>> print new Child()

Super class constructor called.

VDM++では、Childクラスにデフォルトコンストラクタがなくても、実行してくれる。Javaだと、Childクラスに引数ありコンストラクタがあるのにデフォルトコンストラクタがないから、コンパイルが通らない。

番外編

ちなみに、VDM++のコンストラクタで気をつけなければならないケースがある。それはこんなケース。

class Super
  operations
    public Super : seq of char ==> Super
    Super(s) == def - = new IO().echo(s ^ "¥n") in skip;
end Super

class Child is subclass of Super
  instance variables
    i : int := 1;

  operations
    public Child : () ==> Child
    Child() == def - = new IO().echo("Child class constructor called.¥n") in skip;
    
    public getI : () ==> int
    getI() == return i;
end Child

これを、こんな実行するとこうなる。

>> init
>> create child := new Child("aaa")
>> print child.getI()

Run-Time Error 73: 識別子が定義されていないか、初期化されていません

インスタンス変数の初期化がされずに、そのままアクセスするとエラーとなるのだ。

これが起こる条件は以下の通り。

• 親クラスに引数ありのコンストラクタがある
• 子クラスには、親クラスにある引数ありコンストラクタがない
• 親クラスにインスタンス変数がある
• 子クラスのインスタンスを、親クラスにある引数ありコンストラクタで生成する

この問題は、VDM++におけるオブジェクト指向の取り扱い仕様のせい。現在は、こういった問題も含めて、VDMの言語仕様を決めるLanguage Boardがあって、そこで検討しているので、その結果をVDMToolsにもフィードバックしていけるといいね。。