Equational Reasoning about Object-Oriented Programs

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.

The infared optical properties of Sr2RuO4 and SmTiO3 including an object-oriented resistivity interface /

The perovskite crystal structure is host to many different materials from insulating to superconducting providing a diverse range of intrinsic character and complexity. A better fundamental description of these materials in terms of their electronic, optical and magnetic properties undoubtedly precedes an effective realization of their application potential. SmTiOa, a distorted perovskite has a strongly localized electronic structure and undergoes an antiferromagnetic transition at 50 K in its nominally stoichiometric form. Sr2Ru04 is a layered perovskite superconductor (ie. Tc % 1 K) bearing the same structure as the high-tem|>erature superconductor La2_xSrrCu04. Polarized reflectance measurements were carried out on both of these materials revealing several interesting features in the far-infrared range of the spectrum. In the case of SmTiOa, although insulating, evidence indicates the presence of a finite background optical conductivity. As the temperature is lowered through the ordering temperature a resonance feature appears to narrow and strengthen near 120 cm~^ A nearby phonon mode appears to also couple to this magnetic transition as revealed by a growing asymmetry in the optica] conductivity. Experiments on a doped sample with a greater itinerant character and lower Neel temperature = 40 K also indicate the presence of this strongly temperature dependent mode even at twice the ordering temperature. Although the mode appears to be sensitive to the magnetic transition it is unclear whether a magnon assignment is appropriate. At very least, evidence suggests an interesting interaction between magnetic and electronic excitations. Although Sr2Ru04 is highly anisotropic it is metallic in three-dimensions at low temperatures and reveals its coherent transport in an inter-plane Drude-like component to the highest temperatures measured (ie. 90 K). An extended Drude analysis is used to probe the frequency dependent scattering character revealing a peak in both the mass enhancement and scattering rate near 80 cm~* and 100 cm~* respectively. All of these experimental observations appear relatively consistent with a Fermi-liquid picture of charge transport. To supplement the optical measurements a resistivity station was set up with an event driven object oriented user interface. The program controls a Keithley Current Source, HP Nano-Voltmeter and Switching Unit as well as a LakeShore Temperature Controller in order to obtain a plot of the Resistivity as a function of temperature. The system allows for resistivity measurements ranging from 4 K to 290 K using an external probe or between 0.4 K to 295 K using a Helium - 3 Cryostat. Several materials of known resistivity have confirmed the system to be robust and capable of measuring metallic samples distinguishing features of several fiQ-cm.

Winâ Foy : functional object-oriented programming language

This thesis will introduce a new strongly typed programming language utilizing Self types, named Win--*Foy, along with a suitable user interface designed specifically to highlight language features. The need for such a programming language is based on deficiencies found in programming languages that support both Self types and subtyping. Subtyping is a concept that is taken for granted by most software engineers programming in object-oriented languages. Subtyping supports subsumption but it does not support the inheritance of binary methods. Binary methods contain an argument of type Self, the same type as the object itself, in a contravariant position, i.e. as a parameter. There are several arguments in favour of introducing Self types into a programming language (11. This rationale led to the development of a relation that has become known as matching [4, 5). The matching relation does not support subsumption, however, it does support the inheritance of binary methods. Two forms of matching have been proposed (lJ. Specifically, these relations are known as higher-order matching and I-bound matching. Previous research on these relations indicates that the higher-order matching relation is both reflexive and transitive whereas the f-bound matching is reflexive but not transitive (7]. The higher-order matching relation provides significant flexibility regarding inheritance of methods that utilize or return values of the same type. This flexibility, in certain situations, can restrict the programmer from defining specific classes and methods which are based on constant values [21J. For this reason, the type This is used as a second reference to the type of the object that cannot, contrary to Self, be specialized in subclasses. F-bound matching allows a programmer to define a function that will work for all types of A', a subtype of an upper bound function of type A, with the result type being dependent on A'. The use of parametric polymorphism in f-bound matching provides a connection to subtyping in object-oriented languages. This thesis will contain two main sections. Firstly, significant details concerning deficiencies of the subtype relation and the need to introduce higher-order and f-bound matching relations into programming languages will be explored. Secondly, a new programming language named Win--*Foy Functional Object-Oriented Programming Language has been created, along with a suitable user interface, in order to facilitate experimentation by programmers regarding the matching relation. The construction of the programming language and the user interface will be explained in detail.

Object-Oriented Genetic Programming for the Automatic Inference of Graph Models for Complex Networks

Complex networks are systems of entities that are interconnected through meaningful relationships. The result of the relations between entities forms a structure that has a statistical complexity that is not formed by random chance. In the study of complex networks, many graph models have been proposed to model the behaviours observed. However, constructing graph models manually is tedious and problematic. Many of the models proposed in the literature have been cited as having inaccuracies with respect to the complex networks they represent. However, recently, an approach that automates the inference of graph models was proposed by Bailey [10] The proposed methodology employs genetic programming (GP) to produce graph models that approximate various properties of an exemplary graph of a targeted complex network. However, there is a great deal already known about complex networks, in general, and often specific knowledge is held about the network being modelled. The knowledge, albeit incomplete, is important in constructing a graph model. However it is difficult to incorporate such knowledge using existing GP techniques. Thus, this thesis proposes a novel GP system which can incorporate incomplete expert knowledge that assists in the evolution of a graph model. Inspired by existing graph models, an abstract graph model was developed to serve as an embryo for inferring graph models of some complex networks. The GP system and abstract model were used to reproduce well-known graph models. The results indicated that the system was able to evolve models that produced networks that had structural similarities to the networks generated by the respective target models.

The nature of avidyÄ in Buddhism and VedÄ nta

This thesis deals with the nature of ignorance as it was interpreted in the Upani~adic tradition, specifically in Advaita Vedanta, and in early and Mahayana Buddhism , e specially in the Madhyamika school of Buddhism. The approach i s a historical and comparative one. It examines the early thoughts of both the upanis.a ds and Buddhism abou t avidya (ignorance), shows how the notion was treated by the more speculative and philosphically oriented schools which base d themselves on the e arly works, and sees how their views differ. The thesis will show that the Vedinta tended to treat avidya as a topic for metaphysical s peculation as t he s chool developed, drifting from its initial e xistential concerns, while the Madhyamika remained in contact with the e xistential concerns evident in the first discourses of the Buddha. The word "notion" has been chosen for use in referring t o avidya, even though it may have non-intellectual and emotional connotations, to avoid more popular a lternatives such as "concept" or "idea". In neither the Upani,ads, Advaita Vedanta, or Buddhism is ignorance merely a concept or an idea. Only in a secondary sense, in texts and speech , does it become one. Avidya has more to do with the lived situation in which man finds himself, with the subjectobject separation in which he f eels he exists, than with i i i intel lect ual constr ucts . Western thought has begun to r ealize the same with concerns such as being in modern ontology, and has chosen to speak about i t i n terms of the question of being . Avidya, however, i s not a 'question' . If q ue stions we r e to be put regarding the nature of a vidya , they would be more of t he sort "What is not avidya?", though e ven here l anguage bestows a status t o i t which avidya does not have. In considering a work of the Eastern tradition, we f ace t he danger of imposing Western concepts on it. Granted t hat avidya is customari ly r endered i n English as ignorance, the ways i n which the East and West view i gno rance di f f er. Pedagogically , the European cultures, grounded in the ancient Greek culture, view ignorance as a l ack or an emptiness. A child is i gnorant o f certain t hings and the purpose o f f ormal education , in f act if not in theory, is to fill him with enough knowledge so that he can cope wit h t he complexities and the e xpectations of s ociety. On another level, we feel t hat study and research will l ead t o the discovery o f solutions, which we now lack , for problems now defying solut i on . The East, on the o t her hand, sees avidya in a d i fferent light.Ignorance isn't a lack, but a presence. Religious and philosophical l iterature directs its efforts not towards acquiring something new, but at removing t.he ideas and opinions that individuals have formed about themselves and the world. When that is fully accomplished, say the sages , t hen Wisdom, which has been obscured by those opinions, will present itself. Nothing new has to be learned, t hough we do have t o 'learn' that much. The growing interest in t he West with Eastern religions and philosophies may, in time, influence our theoretical and practical approaches to education and learning, not only in the established educati onal institutions, but in religious , p sychological, and spiritual activities as well. However, the requirements o f this thesis do no t permit a formulation of revolutionary method or a call to action. It focuses instead on the textual arguments which attempt to convince readers that t he world in which they take themselves to exist is not, in essence, real, on the ways i n which the l imitations of language are disclosed, and on the provisional and limited schemes that are built up to help students see through their ignorance. The metaphysic s are provisional because they act only as spurs and guides. Both the Upanisadic and Buddhist traditions that will be dealt with here stress that language constantly fails to encompass the Real. So even terms s uch as 'the Real', 'Absolute', etc., serve only to lead to a transcendent experience . The sections dealing with the Upanisads and Advaita Vedanta show some of the historical evolution of the notion of avidya, how it was dealt with as maya , and the q uestions that arose as t o its locus. With Gau?apada we see the beginnings of a more abstract treatment of the topic, and , the influence of Buddhism. Though Sankhara' S interest was primarily directed towards constructing a philosophy to help others attain mok~a ( l iberation), he too introduced t echnica l t e rminology not found in the works of his predecessors. His work is impressive , but areas of it are incomplete. Numbers of his followers tried to complete the systematic presentation of his insi ghts . Their work focuses on expl anat i ons of adhyasa (superimposition ) , t he locus and object of ignorance , and the means by which Brahman takes itself to be the jiva and the world. The section on early Buddhism examines avidya in the context o f the four truths, together with dubkha (suffering), the r ole it p l ays in t he chain of dependent c ausation , a nd t he p r oblems that arise with t he doctrine of anatman. With t he doct rines of e arly Buddhism as a base, the Madhyamika elaborated questions that the Buddha had said t e nded not t o edi f ication. One of these had to do with own - being or svabhava. Thi s serves a s a centr e around which a discussion o f i gnorance unfolds, both i ndividual and coll ective ignorance. There follows a treatment of the cessation of ignorance as it is discussed within this school . The final secti on tries to present t he similarities and differences i n the natures o f ignorance i n t he two traditions and discusses the factors responsible for t hem . ACKNOWLEDGEMENTS I would like to thank Dr. Sinha for the time spent II and suggestions made on the section dealing with Sankara and the Advait.a Vedanta oommentators, and Dr. Sprung, who supervised, direoted, corrected and encouraged the thesis as a whole, but especially the section on Madhyamika, and the final comparison.