Email Gateway (Feb 24 2024 at 10:07): Email Gateway (Feb 24 2024 at 10:07):From: "\"DongZe Su\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I have been recently using autocorres for the formal verification of C
programs, but I am now facing three issues and cannot find the corresponding
documentation or solutions.
Taking the swap function as an example, its proof process is as follows:
lemma “{| λs. is_valid_w32 s a ∧ s[a] = x ∧ is_valid_w32 s b ∧ s[b] = y |}
swap 0 a b {| λ_ s. s[a] = y ∧ s[b] = x |}”
apply (unfold swap’_def)
apply wp
apply clarsimp
apply (simp add: fun-upd-apply)
done
I understand that the lemma is written according to the Hoare logic
precondition and postcondition. However, I couldn't find the detailed
explanation of the {| |} syntax in the current documentation, only the
explanation of [| |]. So I would like to know what the specific meaning of the
syntax used here is.
When verifying a C function that calls other functions in other files, how
should we introduce the definitions of other functions? For example, there is
a function FuncA in FileA.c and a function FuncB in FileB.c, and FuncA calls
FuncB. Using install_c_file FileA.c only reads the definition of FuncA, and
FuncB is recorded as Func_Body_Not_In_Input_C_File. However, if we use
install_c_file FileA.c install_c_file FileB.c it will report an error that
FuncB is defined twice.
Sometimes the Isabelle error messages are very difficult to understand,
especially when using autocorres.
Thanks！
Best regards
Last updated: Apr 29 2024 at 04:18 UTC