Library ProgramStructures

Basic structures used in programs and during runtime. @author Patryk Czarnik

Require Import Common.
Require Import FSets.FMaps.
Require Import FSets.FMapInterface.
Require Import NArith.
Require Import ValuesNTypes.

Program sructures

Module of this type provides structures that are used in static program representation (class etc.) as well as in dynamic runtime structures and semantics. Namely, they are:
  • program counter (PC) with offset,
  • variable indices.
Module Type PROGRAM_STRUCTURES.

Included modules

  Declare Module M_ValuesAndTypes : VALUES_AND_TYPES.
  Import M_ValuesAndTypes.

  Open Local Scope type_scope.

Method signature consists of method name, the fact if the method is static, and a list of argument types. Arguments are given in reversed order: the last argument is the head of the list. Method signatures are unique within classes.
  Definition TSignature: Set := TShortName × list TType.

Qualified method name uniquely (? class-loadres ?) identifies a method within a program.
  Definition TQualifiedMethodName: Set := TClassName × TSignature.

Program counters and offsets

Moved to ValuesNTypes.

Variable indices

Local variable index.
  Parameter TVar: Set.

Equality on variable indices is decidable.
  Axiom PVar_eqDec: eqDecS TVar.

TVar is isomorphic to the set of natural nubers.
  Parameter varFromNat: nat → TVar.
  Parameter varToNat: TVar → nat.
  Axiom PvarNat: ∀ var, varFromNat (varToNat var) = var.
  Axiom PnatVar: ∀ n, varToNat (varFromNat n) = n.

  Parameter nextVar: TVar → TVar.

  Axiom PnextVarSucc: ∀ var, varToNat (nextVar var) = S (varToNat var).

End PROGRAM_STRUCTURES.

Program structures enriched with maps on TPC and TVar

Module of this type implements PROGRAM_STRUCTURES and, additionally, provides total order on TPC and TVar and maps with TPC or TVar as keys.
Module Type PROGRAM_STRUCTURES_WITH_MAP.

PROGRAM_STRUCTURES

This signature extends PROGRAM_STRUCTURES.
  Include PROGRAM_STRUCTURES.
  Import M_ValuesAndTypes.

Maps


TVar as OrderedType.
  Declare Module M_Var_as_OT: OrderedType with
    Definition t := TVar
    with Definition eq := @eq TVar.

A FMap with keys from TVar.
  Declare Module M_VarMap: S
    with Module E := M_Var_as_OT.
End PROGRAM_STRUCTURES_WITH_MAP.

Module ProgramStructuresFacts
  (_ProgramStructures: PROGRAM_STRUCTURES).
  Import _ProgramStructures.M_ValuesAndTypes.
  Import _ProgramStructures.

  Definition var0 := varFromNat 0.
  Definition var1 := varFromNat 1.
  Definition var2 := varFromNat 2.
  Definition var3 := varFromNat 3.

  Lemma distinct_varFromNat: ∀ n1 n2: nat,
    n1 ≠ n2 → varFromNat n1 ≠ varFromNat n2.
  Proof.
    intuition.
    apply H; clear H.
    rewrite <- (PnatVar n1).
    rewrite <- (PnatVar n2).
    f_equal.
    assumption.
  Qed.

  Lemma distinct_vars_0_1: var0 ≠ var1.
  Proof.
    apply distinct_varFromNat.
    auto.
  Qed.
  Lemma distinct_vars_0_2: var0 ≠ var2.
  Proof.
    apply distinct_varFromNat.
    auto.
  Qed.
  Lemma distinct_vars_0_3: var0 ≠ var3.
  Proof.
    apply distinct_varFromNat.
    auto.
  Qed.
  Lemma distinct_vars_1_2: var1 ≠ var2.
  Proof.
    apply distinct_varFromNat.
    auto.
  Qed.
  Lemma distinct_vars_1_3: var1 ≠ var3.
  Proof.
    apply distinct_varFromNat.
    auto.
  Qed.
  Lemma distinct_vars_2_3: var2 ≠ var3.
  Proof.
    apply distinct_varFromNat.
    auto.
  Qed.

  Lemma distinct_vars_next: ∀ var, var ≠ nextVar var.
  Proof.
    intros.
    rewrite <- (PvarNat (nextVar var)).
    rewrite PnextVarSucc.
    rewrite <- (PvarNat var) at 1.
    apply distinct_varFromNat.
    auto.
  Qed.

  Module StandardNames.
    Parameter Object: TClassName.
    Parameter Throwable: TClassName.
    Parameter NullPointerException: TClassName.
    Parameter ArrayIndexOutOfBoundsException: TClassName.
    Parameter ArrayStoreException: TClassName.
    Parameter NegativeArraySizeException: TClassName.
    Parameter ClassCastException: TClassName.
    Parameter AbstractMethodError: TClassName.
    Parameter ArithmeticException: TClassName.
    Parameter IllegalMonitorStateException: TClassName.

    Definition arrayInterfaces: list TClassName := nil.

  End StandardNames.
End ProgramStructuresFacts.