Compilation to Javascript

[JlnWntr]

Dafny version

4.11.0

Code to produce this issue

module Collision {
  class Box {
    var x: real
    var y: real
    var w: real
    var h: real
    var last_x: real
    var last_y: real

    constructor (x: real, y:real, w:real, h:real) {
      this.x := x;
      this.y := y;
      this.w := w;
      this.h := h;
      this.last_x := 0.0;
      this.last_y := 0.0;
    }

  method move(x: real, y:real) 
    modifies this
    {
     this.x := x;
     this.y := y;
    }
}

Command to run and resulting output

dafny build --target:js test.dfy

What happened?

This Dafny code:

class Box {
    var x: real
    var y: real
    var w: real
    var h: real
    var last_x: real
    var last_y: real

    constructor (x: real, y:real, w:real, h:real) {
      this.x := x; this.y := y;
      this.w := w;   this.h := h;
      this.last_x := 0.0;   this.last_y := 0.0;
    }
}

produces this javascript-code:

$module.Box = class Box {
    constructor () {
      this._tname = "Test.Box";
      this.x = _dafny.BigRational.ZERO;
      this.y = _dafny.BigRational.ZERO;
      this.w = _dafny.BigRational.ZERO;
      this.h = _dafny.BigRational.ZERO;
      this.last__x = _dafny.BigRational.ZERO;
      this.last__y = _dafny.BigRational.ZERO;
    }

How can you create with this a "box" in your javascript-code with the actual values?

What type of operating system are you experiencing the problem on?

Mac, Linux