Theory sum_list

section ‹ Example: Summing a List ›

theory sum_list
  imports "../utp_easy_parser"
begin

text ‹ This theory exemplifies the use of the Isabelle/UTP Hoare logic verification component. 
  We first create a state space with the variables the program needs. ›

alphabet st_sum_list = 
  i   :: nat
  xs  :: "int list"
  ans :: int

text ‹ Next, we define the program as by a homogeneous relation over the state-space type. ›

abbreviation Sum_List :: "st_sum_list hrel" where
  "Sum_List ≡
  i := 0 ;;
  ans := 0 ;;
  while (i < #xs) invr (ans = list_sum(take(i, xs)))
  do
    ans := ans + xs[i] ;;
    i := i + 1
  od"

text ‹ Next, we symbolically evaluate some examples. ›

lemma "TRY([&xs ↦⇩s «[4,3,7,1,12,8]»] ⊨ Sum_List)"
  apply (sym_eval) oops

text ‹ Finally, we verify the program. ›

theorem Sum_List_sums:
  "{{xs = «XS»}} Sum_List {{ans = list_sum(xs)}}"
  by (hoare_auto, metis add.foldr_snoc take_Suc_conv_app_nth)

end