1 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
2 <link rel="stylesheet" href="style.css" type="text/css"/>
3 <script src="code.js" type="text/javascript"></script>
5 <h1>strlen proven, but not by me</h1>
8 size_t strlen(const char *s)
11 /*@ loop invariant s <= sc <= s + strlen(s);
12 loop invariant valid_str(sc);
13 loop invariant strlen(s) == strlen(sc) + (sc - s);
15 loop variant strlen(s) - (sc - s);
17 for (sc = s; *sc != '\0'; ++sc)
24 Where is the <code>/*@</code> comment for this function?
25 We’ll come to that in a minute ...
29 <p class="attribution">
30 Proof by Denis Efremov, Ivannikov Institute for System Programming
31 at the Russian Academy of Sciences,
32 <a href="https://github.com/evdenis/verker/blob/master/src/strlen.c">https://github.com/evdenis/verker/blob/master/src/strlen.c</a>