why3/examples_in_progress/ladderstring.mlw

module LadderStringMelseqiQR
  (* According to MELSEQ iQ-R programming manual *)

  use string.String as S
  use int.Int

  type astring = String string
               | WString string
  (** type for MELSEQ iQ-R any_string *)

  type aint = int
  (** type for MELSEQ iQ-R any_int TODO *)

  let function string_of_astring (s: astring) =
    match s with
    | String s -> s
    | WString s -> s
    end
  meta coercion function string_of_astring

  predicate satisfy_size (s: astring) =
    match s with
    | String s -> S.length s <= 255
    | WString s -> S.length s < 128
    end

  val function length (s: astring) : aint
    requires {satisfy_size s}
    ensures  {result = S.length s}

  val function left (s: astring) (x: aint)   : astring
    requires {satisfy_size s}
    requires {0 <= x < S.length s}
    ensures  {result = S.substring s 0 x}

  val function right (s: astring) (x: aint)   : astring
    requires {satisfy_size s}
    requires {0 <= x <= S.length s}
    ensures  {result = S.substring s (S.length s - x) x}

  val function middle (s: astring) (x i: aint) : astring
    requires {satisfy_size s}
    requires {0 < i <= S.length s}
    requires {0 <= x <= S.length s - i + 1}
    ensures  {result = S.substring s (i-1) x}

  val function concat2 (s1 s2: astring) : astring
    requires {satisfy_size s1 && satisfy_size s2}
    ensures  {result = S.substring (S.concat s1 s2) 0 256}
             (* TODO check if this actually happens in iQ-R *)

  val function concat3 (s1 s2 s3: astring) : astring
    requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3}
    ensures  {result = S.substring (S.concat (S.concat s1 s2) s3) 0 256}
             (* TODO check if this actually happens in iQ-R *)

  val function concat4 (s1 s2 s3 s4: astring) : astring
    requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3 &&
              satisfy_size s4}
    ensures  {result = S.substring (S.concat (S.concat s1 s2) (S.concat s3 s4)) 0 256}
             (* TODO check if this actually happens in iQ-R *)

  val function concat5 (s1 s2 s3 s4 s5: astring) : astring
    requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3 &&
              satisfy_size s4 && satisfy_size s5}
    ensures  {result =
      S.substring (S.concat (S.concat s1 s2) (S.concat s3 (S.concat s4 s5))) 0 256}
             (* TODO check if this actually happens in iQ-R *)

  val function insert  (s1: astring) (s2: astring) (i: aint) : astring
    requires {satisfy_size s1 && satisfy_size s2}
    requires {0 < i <= S.length s1}
    requires {length s1 + length s2 < 256}
    ensures  {result = S.concat (S.concat (S.substring s1 0 i)
                                          s2)
                                (S.substring s1 i (length s1))}

  val function delete (s:  astring) (x i: aint) : astring
    requires {satisfy_size s}
    requires {0 < i < S.length s}
    requires {0 <= x <= S.length s - i + 1}
    ensures  {result = S.concat (S.substring s 0 (i - 1))
                                 (S.substring s (i + x - 1)
                                                (S.length s - i - x + 1))}

  val function replace (s1: astring) (s2: astring) (x i: aint) : astring
    requires {satisfy_size s1 && satisfy_size s2}
    requires {0 < i < S.length s1}
    requires {0 <= x <= length s1 - i + 1}
    requires {S.length s2 >= x}
    (* this is not part of MELSEQ iQ-R manual, but the simulator seems
       to have this behavior *)
    ensures {result = S.concat (S.concat (S.substring s1 0 i)
                                         (S.substring s2 0 x))
                               (S.substring s1 (i + x - 1) (S.length s1))}

  val function find (s1: astring) (s2: astring) : aint
    requires {satisfy_size s1 && satisfy_size s2}
    ensures  {result = S.indexof s1 s2 0 + 1}

end

(* module LadderString1 (* According to IEC 61131-3 *) *)

(*   type char *)
(*   type wchar *)
(*   type string *)
(*   type wstring *)

(*   type any_char   = Char char *)
(*                   | WChar wchar *)
(*   type any_string = String string *)
(*                   | WString wstring *)
(*   type any_chars  = AChar any_char *)
(*                   | AString any_string *)

(*   type any_int *)

(*   function len     (s: any_string) : any_int *)
(*   function left    (s: any_string) (i: any_int)   : any_string *)
(*   function right   (s: any_string) (i: any_int)   : any_string *)
(*   function middle  (s: any_string) (i o: any_int) : any_string *)
(*   function concat2 (s1 s2: any_chars) : any_string *)
(*   function concat3 (s1 s2 s3: any_chars) : any_string *)
(*   function concat4 (s1 s2 s3 s4: any_chars) : any_string *)
(*   function concat5 (s1 s2 s3 s4 s5: any_chars) : any_string *)
(*   function insert  (s1: any_string) (s2: any_chars) (i: any_int) : any_string *)
(*   function delete  (s:  any_string) (o i: any_int) : any_string *)
(*   function replace (s1: any_string) (s2: any_chars) (o i: any_int) : any_string *)
(*   function find    (s1: any_string) (s2: any_chars) : any_int *)
(* end *)

(* module LaddeeString2 *)

(*   type char *)
(*   type wchar *)
(*   type string *)
(*   type wstring *)

(*   function len     (s: wstring) : int *)
(*   function left    (s: wstring) (i: int) : wstring *)
(*   function right   (s: wstring) (i: int) : wstring *)
(*   function middle  (s: wstring) (i o: int) : wstring *)
(*   function concat2 (s1 s2: wstring) : wstring *)
(*   function concat3 (s1 s2 s3: wstring) : wstring *)
(*   function concat4 (s1 s2 s3 s4: wstring) : wstring *)
(*   function concat5 (s1 s2 s3 s4 s5: wstring) : wstring *)
(*   function insert  (s1 s2: wstring) (i: int) : wstring *)
(*   function delete  (s:  wstring) (o i: int) : wstring *)
(*   function replace (s1 s2: wstring) (o i: int) : wstring *)
(*   function find    (s1 s2: wstring) : int *)
(* end *)