3 resultados para Computer software -- Verification
em Brock University, Canada
Resumo:
Formal 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.
Resumo:
Lichenologists and users of lichenometry have long used calipers or photogrammetry to measure the growth of crustose lichens. Now, digital photography and popular computer software provide methodological alternatives. This thesis developed and tested a new methodology for tracking change and growth of the lichen, Rhizocarpon geographicum. Adobe Photoshop CS3 Extended software and a photographic time series (1996,2003,2006 and 2007) were used to measure thallus diameter, area, prothallus width and areolae area in 115 small R. geographicum thalli (0.53-1049.88 mm2 ). Measures of 8 diameters per thallus showed that change in diameter was highly variable and is a weak index of growth. Thallus area was a reliable measure of growth (power correlation, R2 = 0.89). Rapid, highly irregular growth occurred in small thalli «30 mm2 ), and steady, uniform growth occurred in larger thalli (>30 mm2 ). This new methodology is tedious but can potentially generate accurate and precise measures for even the tiniest of lichens.
Resumo:
The aim of this thesis is to explore the relationship between imagery, technology, and remote adult Aboriginal teacher candidates through the computer software Elluminate Live. It focuses on the implications that the role imagery plays in third generation distance education with these learners and the new media associated therein. The thesis honours the Medicine Wheel teachings and is presented within this cyclical framework that reflects Indigenous philosophies and belief systems. In accordance, Sharing Circle as methodology is used to keep the research culturally grounded, and tenets of narrative inquiry further support the study. Results indicate there are strong connections to curricula enhanced with imagery—most notably a spiritual connection. Findings also reveal that identity associated to geographical location is significant, as are supportive networks. Third generation distance education, such as Elluminate Live, needs to be addressed before Aboriginal communities open the doors to all it encompasses, and although previous literature peers into various elements, this study delves into why the graphical interface resonates with members of these communities. Of utmost importance is the insight this thesis lends to the pedagogy that may possibly evoke a transformative learning process contributing to the success rate of Aboriginal learners and benefit Aboriginal communities as a whole.