Return to the
comp.compilers page.
Search the
comp.compilers archives again.
| Related articles |
|---|
| Re: C arithmetic, was Software proofs, was Are there different Keith.S.Thompson+u@gmail.com (Keith Thompson) (2023-02-05) |
| Re: C arithmetic, was Software proofs, was Are there different gah4@u.washington.edu (gah4) (2023-02-06) |
| Re: C arithmetic, was Software proofs, was Are there different DrDiettrich1@netscape.net (Hans-Peter Diettrich) (2023-02-07) |
| Re: C arithmetic, was Software proofs, was Are there different gah4@u.washington.edu (gah4) (2023-02-08) |
| Re: C arithmetic, was Software proofs, was Are there different anton@mips.complang.tuwien.ac.at (2023-02-08) |
| Re: C arithmetic, was Software proofs, was Are there different DrDiettrich1@netscape.net (Hans-Peter Diettrich) (2023-02-08) |
| Re: C arithmetic, was Software proofs, was Are there different gah4@u.washington.edu (gah4) (2023-02-09) |
| [6 later articles] |
| From: | Martin Ward <mwardgkc@gmail.com> |
| Newsgroups: | comp.compilers |
| Date: | Tue, 31 Jan 2023 14:04:39 +0000 |
| Organization: | Compilers Central |
| Injection-Info: | gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="50034"; mail-complaints-to="abuse@iecc.com" |
| Keywords: | translator, theory |
| Posted-Date: | 31 Jan 2023 12:58:22 EST |
On 30/01/2023 10:00, John Levine wrote:
> [Remember that while the halting problem is insoluble in general, it's
> often soluble in specific cases, e.g. "halt" or "foo: goto foo".
More usefully, there are methods for transforming a formal
specification into an executable implementation which
preserve semantic equivalence, and therefore are guaranteed
to produce a terminating program (for input states for which
the specification is defined). For example:
"Provably Correct Derivation of Algorithms Using FermaT"
Martin Ward and Hussein Zedan
Formal Aspects of Computing, September 2014.
Volume 26, Issue 5, Pages 993--1031, 2014-09-01, ISSN: 0934-5043
doi:dx.doi.org/10.1007/s00165-013-0287-2
http://www.gkc.org.uk/martin/papers/trans-prog-t.pdf
> Nevertheless, I would be quite surprised if anyone could prove a
> non-toy translator correct. -John]
According to this paper: "The state of the art [as of 2014] is
the CompCert compiler, which compiles almost all of the C language
to PowerPC, ARM and x86 assembly and has been mechanically verified
using the Coq proof assistant."
Xavier Leroy. "Formally verifying a compiler: Why? How? How far?".
CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code
Generation and Optimization, Apr 2011, Chamonix, France.
⟨10.1109/CGO.2011.5764668⟩. ⟨hal-01091800⟩
https://hal.inria.fr/hal-01091800
--
Martin
Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4
Return to the
comp.compilers page.
Search the
comp.compilers archives again.