SSL arrays_examples.pvs   Sprache: unbekannt

arrays_examples: THEORY
BEGIN
  
  IMPORTING arrays

  R0 : Reals[10] = init   % Initializes an array of 10 reals with 0
  R1 : Reals[10] = init_with(1)  % Initializes an array of 10 reals with 1
  B0 : Bools[10] = init   % Initializes an array of 10 Booleans with FALSE
  B1 : Bools[10] = init_with(TRUE) % Initializes an array of 10 Booleans with TRUE
  S0 : Strings[10] = init % Initializes an array of 10 strings with ""
  S1 : Strings[10] = init_with("X") % Initializes an array of 10 strings with "X"
  N : Nats[10] = init     % Initializes an array of 10 natural numbers with 0
  Z : Ints[10] = init     % Initializes an array of 10 integers with 0
  Q : Rats[10] = init     % Initializes an array of 10 rational numbers with 0

  NS0 : ArrayOf[10][[nat,string]] = init_with[10][[nat,string]]((0,""))  % Initializes an array of 10 pairs [nat,string] with (0,"")
  NS1 : ArrayOf[10][[nat,string]] = NS0 WITH [`1 := (1,"")] % Same as NS0 except that it has (1,"") in 1st position
  
  GridPoint : TYPE = [# x,y:int #] 
  origin : GridPoint = (# x := 0, y := 0 #)
  RR0 : ArrayOf[10][GridPoint] = init_with[10][GridPoint](origin) % Initializes an array of 10 grid points with origin
  RR1 : ArrayOf[10][GridPoint] = RR0 WITH [`1 := (# x := 1, y:= 0 #)] % Same as RR0 except that it has the point (1,0) in 1st position

END arrays_examples