/* A simple, incomplete implementation of a nettrek-like two dimensional
   shooting game.  Written in a Java-like pseudo code.
   It's purpose is to illustrate preconditions, postconditions, loop
   variants and invariants and class invariants.

Parameters
  - Ships fight in a 2D plane with guns and missiles
  - (0,0) is a the bottom left of the screen.  X-axis extends to the right,
    Y-axis towards the monitor top.
  - (1000,800) is the maximum (X, Y) position respectively  
  - Ships must stay within the map bounds at all times
  
  - There are 6 classes of ships, 1 to 6
    - 1 is the smallest, 6 the largest    
  - A ship has [Ship class] - 2 (min 0) missile launchers
    - Reload time of 5 seconds    - Hit for 100 damage
    - Range is 300 pixels
  - A ship has [Ship class] guns
    - Reload time of 3 seconds    - Hit for 50 damage
    - Range is 100 pixels
  - Ships have [Ship class] * 100 hull points
    - They are destroyed at <= 0
  - Shields have [Ship class] * 150 points
    - Shields regenerate 1% of their damage per second
  - Maximum ship speed is (8 - ShipClass) * 50 pixels/second in the x
    and y axis
    - Note that ship class 1 is the fastest
    - Acceleration is instantaneous
    
*/
  

class NShip {

String shipName;
int shipClass, hullPointsMax, shieldPointsMax;
int hullPoinsCurrent, shieldPointsCurrent;
int[] missReloadTime, gunsReloadTime;
int xPos, yPos, xVelocity, yVelocity;
boolean imAlive;

  /* ===============================================================
  Create a ship.  Set the hull and shields to max values and the
  reload times to zero.  Randomly assign the ship's position. */

  constructor Create(int inShipClass, String inShipName) {
    // Preconditions for a constructor?

    imAlive = True;
    shipClass = inShipClass;
    hullPointsMax = inShipClass * 100;
    ...
    missReloadTime = new int[inShipClass - 2];
    for (int i = 0; i < inShipClass - 2; i++)
      missReloadTime[i] = 0;
    ...  
    xPos = random(1000);
    xVelocity = 0;
    ...

    // post
  }

  /* ============================================================ */

  void SetVelocity(int inXVel, inYVel)
  {
    // pre
  
    xVelocity = inXVel;
    ...
  
    // post
  }

  /* ===============================================================
  Move xVelocity and yVelocity pixels.  +x is to the right, +y up.*/

  void Move() {
    // pre

    ...
    xPox := ...
    yPos := ...

    // post
  }

  /* ===============================================================
  Another player has hit you for inDamage damage */

  void ImHit(int inDamage) {
    // pre
    
    ...
    
    // post
  }

  /* ============================================================ */

  boolean AmIAlive()
  {
    // pre

    imAlive = (HullPoints > 0);
    return imAlive;

    // post
  }

  /* ===============================================================
  reload time must be 0 for a gun to shoot */

  void CanIShootGun(int inGunNo) {
    // pre

    return gunsReloadTime[inGunNo] == 0;

    // post
  }

  /* ===============================================================
  Are any enemy ships in range of our guns? */

  boolean AnyEnemiesInGunRange(NShip[] inShips ) {
    // pre
    bool InRange = false;

    for (int i = 0; i <= inShips.Size - 1; i++) {
      // Invariant
      // Variant
      ... 
    }

    return InRange;
    // post 
  }

  /* ============================================================ */
  // Class invariants go here

  ...

} // NShip