It is hard to ensure correctness as software grows more complex. There are many ways to tackle this problem. Improved documentation can prevent misunderstandings what an interface does. Well built abstractions can prevent some kinds of misuse. Tests can find errors, but unless they are exhaustive, they can never guarantee the absence of errors. The use of formal methods can improve the reliability of software. This work uses the Why3 program verification platform to produce Rust code. Possible semantic-preserving mappings from WhyML to Rust are evaluated, and a subset of the mappings are automated using Why3's extraction framework.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:ltu-73510 |
| Date | January 2019 |
| Creators | Fitinghoff, Nils |
| Publisher | Luleå tekniska universitet, Institutionen för system- och rymdteknik |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0121 seconds