examples_in_progress/ladderstring.mlw

   1 module LadderStringMelseqiQR
   2   (* According to MELSEQ iQ-R programming manual *)
   3
   4   use string.String as S
   5   use int.Int
   6
   7   type astring = String string
   8                | WString string
   9   (** type for MELSEQ iQ-R any_string *)
  10
  11   type aint = int
  12   (** type for MELSEQ iQ-R any_int TODO *)
  13
  14   let function string_of_astring (s: astring) =
  15     match s with
  16     | String s -> s
  17     | WString s -> s
  18     end
  19   meta coercion function string_of_astring
  20
  21   predicate satisfy_size (s: astring) =
  22     match s with
  23     | String s -> S.length s <= 255
  24     | WString s -> S.length s < 128
  25     end
  26
  27   val function length (s: astring) : aint
  28     requires {satisfy_size s}
  29     ensures  {result = S.length s}
  30
  31   val function left (s: astring) (x: aint)   : astring
  32     requires {satisfy_size s}
  33     requires {0 <= x < S.length s}
  34     ensures  {result = S.substring s 0 x}
  35
  36   val function right (s: astring) (x: aint)   : astring
  37     requires {satisfy_size s}
  38     requires {0 <= x <= S.length s}
  39     ensures  {result = S.substring s (S.length s - x) x}
  40
  41   val function middle (s: astring) (x i: aint) : astring
  42     requires {satisfy_size s}
  43     requires {0 < i <= S.length s}
  44     requires {0 <= x <= S.length s - i + 1}
  45     ensures  {result = S.substring s (i-1) x}
  46
  47   val function concat2 (s1 s2: astring) : astring
  48     requires {satisfy_size s1 && satisfy_size s2}
  49     ensures  {result = S.substring (S.concat s1 s2) 0 256}
  50              (* TODO check if this actually happens in iQ-R *)
  51
  52   val function concat3 (s1 s2 s3: astring) : astring
  53     requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3}
  54     ensures  {result = S.substring (S.concat (S.concat s1 s2) s3) 0 256}
  55              (* TODO check if this actually happens in iQ-R *)
  56
  57   val function concat4 (s1 s2 s3 s4: astring) : astring
  58     requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3 &&
  59               satisfy_size s4}
  60     ensures  {result = S.substring (S.concat (S.concat s1 s2) (S.concat s3 s4)) 0 256}
  61              (* TODO check if this actually happens in iQ-R *)
  62
  63   val function concat5 (s1 s2 s3 s4 s5: astring) : astring
  64     requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3 &&
  65               satisfy_size s4 && satisfy_size s5}
  66     ensures  {result =
  67       S.substring (S.concat (S.concat s1 s2) (S.concat s3 (S.concat s4 s5))) 0 256}
  68              (* TODO check if this actually happens in iQ-R *)
  69
  70   val function insert  (s1: astring) (s2: astring) (i: aint) : astring
  71     requires {satisfy_size s1 && satisfy_size s2}
  72     requires {0 < i <= S.length s1}
  73     requires {length s1 + length s2 < 256}
  74     ensures  {result = S.concat (S.concat (S.substring s1 0 i)
  75                                           s2)
  76                                 (S.substring s1 i (length s1))}
  77
  78   val function delete (s:  astring) (x i: aint) : astring
  79     requires {satisfy_size s}
  80     requires {0 < i < S.length s}
  81     requires {0 <= x <= S.length s - i + 1}
  82     ensures  {result = S.concat (S.substring s 0 (i - 1))
  83                                  (S.substring s (i + x - 1)
  84                                                 (S.length s - i - x + 1))}
  85
  86   val function replace (s1: astring) (s2: astring) (x i: aint) : astring
  87     requires {satisfy_size s1 && satisfy_size s2}
  88     requires {0 < i < S.length s1}
  89     requires {0 <= x <= length s1 - i + 1}
  90     requires {S.length s2 >= x}
  91     (* this is not part of MELSEQ iQ-R manual, but the simulator seems
  92        to have this behavior *)
  93     ensures {result = S.concat (S.concat (S.substring s1 0 i)
  94                                          (S.substring s2 0 x))
  95                                (S.substring s1 (i + x - 1) (S.length s1))}
  96
  97   val function find (s1: astring) (s2: astring) : aint
  98     requires {satisfy_size s1 && satisfy_size s2}
  99     ensures  {result = S.indexof s1 s2 0 + 1}
 100
 101 end
 102
 103 (* module LadderString1 (* According to IEC 61131-3 *) *)
 104
 105 (*   type char *)
 106 (*   type wchar *)
 107 (*   type string *)
 108 (*   type wstring *)
 109
 110 (*   type any_char   = Char char *)
 111 (*                   | WChar wchar *)
 112 (*   type any_string = String string *)
 113 (*                   | WString wstring *)
 114 (*   type any_chars  = AChar any_char *)
 115 (*                   | AString any_string *)
 116
 117 (*   type any_int *)
 118
 119 (*   function len     (s: any_string) : any_int *)
 120 (*   function left    (s: any_string) (i: any_int)   : any_string *)
 121 (*   function right   (s: any_string) (i: any_int)   : any_string *)
 122 (*   function middle  (s: any_string) (i o: any_int) : any_string *)
 123 (*   function concat2 (s1 s2: any_chars) : any_string *)
 124 (*   function concat3 (s1 s2 s3: any_chars) : any_string *)
 125 (*   function concat4 (s1 s2 s3 s4: any_chars) : any_string *)
 126 (*   function concat5 (s1 s2 s3 s4 s5: any_chars) : any_string *)
 127 (*   function insert  (s1: any_string) (s2: any_chars) (i: any_int) : any_string *)
 128 (*   function delete  (s:  any_string) (o i: any_int) : any_string *)
 129 (*   function replace (s1: any_string) (s2: any_chars) (o i: any_int) : any_string *)
 130 (*   function find    (s1: any_string) (s2: any_chars) : any_int *)
 131 (* end *)
 132
 133 (* module LaddeeString2 *)
 134
 135 (*   type char *)
 136 (*   type wchar *)
 137 (*   type string *)
 138 (*   type wstring *)
 139
 140 (*   function len     (s: wstring) : int *)
 141 (*   function left    (s: wstring) (i: int) : wstring *)
 142 (*   function right   (s: wstring) (i: int) : wstring *)
 143 (*   function middle  (s: wstring) (i o: int) : wstring *)
 144 (*   function concat2 (s1 s2: wstring) : wstring *)
 145 (*   function concat3 (s1 s2 s3: wstring) : wstring *)
 146 (*   function concat4 (s1 s2 s3 s4: wstring) : wstring *)
 147 (*   function concat5 (s1 s2 s3 s4 s5: wstring) : wstring *)
 148 (*   function insert  (s1 s2: wstring) (i: int) : wstring *)
 149 (*   function delete  (s:  wstring) (o i: int) : wstring *)
 150 (*   function replace (s1 s2: wstring) (o i: int) : wstring *)
 151 (*   function find    (s1 s2: wstring) : int *)
 152 (* end *)