On 2016/07/19 23:42 +0900, Akira Yokosawa wrote:
Hi Paul,
These are typos I noticed while reading recently updated part in "formal/formal.tex".
> Furthermore, although the L4 microkernel is a large software
> artifact from the viewpoint of formal verification, it is tiny
> - compared to the a great number of projects, including LLVM,
> + compared to a great number of projects, including LLVM,
Here, "the" and "a" are redundant. I removed "the", because I have no idea
how many projects are there in this context.
> gcc, the Linux kernel, Hadoop, MongoDB, and a great many others.
>
> Although formal verification is finally starting to show some
> @@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than
> a mechanical proof for a complex implementation!
>
> And the open challenge to those working on formal verification techniques
> -and systems is prove this summary wrong!
> +and systems is to prove this summary wrong!
>
This seems a trivial one.
Thanks, Akira
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
