zenon/formal-methods-fstar
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add Termination

Browse Source
This commit is contained in:
Tobias Eidelpes 2021-06-03 10:35:09 +02:00
parent 7f9fa7758e
commit f1f1e42bc0
1 changed files with 15 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
Project2.fst
View File

@ -174,9 +174,23 @@ let rec nsteps n te cs =
(* Our goal is to prove the termination of this function *) (* Our goal is to prove the termination of this function *)
(* To this end, define a function the following function on callstacks that assigns a measure (in terms of a list of naturals that gets lexicographically interpreted) to each call stack *) (* To this end, define a function the following function on callstacks that assigns a measure (in terms of a list of naturals that gets lexicographically interpreted) to each call stack *)
val gas: plaincallstack -> Tot nat
let gas cs =
match cs with
| (((gas, _, _, _), _, _)::_) -> gas
| _ -> 0
val getDecArgList: (cs: callstack {wellformed cs}) -> Tot (list nat) val getDecArgList: (cs: callstack {wellformed cs}) -> Tot (list nat)
let getDecArgList (cs: callstack {wellformed cs}) = let getDecArgList (cs: callstack {wellformed cs}) =
magic () [ (match cs with
| Exec ps -> gas ps
| Ter (HaltState _ _ g) _ -> g
| Ter ExcState _ -> 0)
; size cs
; match cs with
| Exec _ -> 1
| Ter _ _ -> 0
]
(* A simple helper function that converts a list to a lexicgraphical ordering *) (* A simple helper function that converts a list to a lexicgraphical ordering *)
val getLexFromList: (list nat) -> Tot (lex_t) val getLexFromList: (list nat) -> Tot (lex_t)