Show simple item record

dc.contributor.authorHossain, Md. Nour
dc.date.accessioned2013-04-08T16:27:00Z
dc.date.available2013-04-08T16:27:00Z
dc.date.issued2013-04-08
dc.identifier.urihttp://hdl.handle.net/10464/4258
dc.description.abstractFormal verification of software can be an enormous task. This fact brought some software engineers to claim that formal verification is not feasible in practice. One possible method of supporting the verification process is a programming language that provides powerful abstraction mechanisms combined with intensive reuse of code. In this thesis we present a strongly typed functional object-oriented programming language. This language features type operators of arbitrary kind corresponding to so-called type protocols. Sub classing and inheritance is based on higher-order matching, i.e., utilizes type protocols as basic tool for reuse of code. We define the operational and axiomatic semantics of this language formally. The latter is the basis of the interactive proof assistant VOOP (Verified Object-Oriented Programs) that allows the user to prove equational properties of programs interactively.en_US
dc.subjectSoftware verificationen_US
dc.subjectComputer programming languageen_US
dc.titleEquational Reasoning about Object-Oriented Programsen_US
dc.degree.nameM.Sc. Computer Scienceen_US
dc.degree.levelMastersen_US
dc.contributor.departmentDepartment of Computer Scienceen_US
dc.degree.disciplineFaculty of Mathematics and Scienceen_US
dc.embargo.termsNoneen_US
refterms.dateFOA2021-08-08T01:49:44Z


Files in this item

Thumbnail
Name:
Brock_Hossain_Md._Nour_2011.pdf
Size:
1.406Mb
Format:
PDF

This item appears in the following Collection(s)

Show simple item record