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.

An Interactive Theorem Prover for First-Order Dynamic Logic

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.

Region Connection Calculus: Composition Tables and Constraint Satisfaction Problems

Qualitative spatial reasoning (QSR) is an important field of AI that deals with qualitative aspects of spatial entities. Regions and their relationships are described in qualitative terms instead of numerical values. This approach models human based reasoning about such entities closer than other approaches. Any relationships between regions that we encounter in our daily life situations are normally formulated in natural language. For example, one can outline one's room plan to an expert by indicating which rooms should be connected to each other. Mereotopology as an area of QSR combines mereology, topology and algebraic methods. As mereotopology plays an important role in region based theories of space, our focus is on one of the most widely referenced formalisms for QSR, the region connection calculus (RCC). RCC is a first order theory based on a primitive connectedness relation, which is a binary symmetric relation satisfying some additional properties. By using this relation we can define a set of basic binary relations which have the property of being jointly exhaustive and pairwise disjoint (JEPD), which means that between any two spatial entities exactly one of the basic relations hold. Basic reasoning can now be done by using the composition operation on relations whose results are stored in a composition table. Relation algebras (RAs) have become a main entity for spatial reasoning in the area of QSR. These algebras are based on equational reasoning which can be used to derive further relations between regions in a certain situation. Any of those algebras describe the relation between regions up to a certain degree of detail. In this thesis we will use the method of splitting atoms in a RA in order to reproduce known algebras such as RCC15 and RCC25 systematically and to generate new algebras, and hence a more detailed description of regions, beyond RCC25.

L-Fuzzy Relations in Coq

Heyting categories, a variant of Dedekind categories, and Arrow categories provide a convenient framework for expressing and reasoning about fuzzy relations and programs based on those methods. In this thesis we present an implementation of Heyting and arrow categories suitable for reasoning and program execution using Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy relations, category theory and dependent type theory before describing our implementation. In addition, we provide examples of program executions based on our framework.

Perceptions of some teachers about the similarities and/or differences in teaching online versus in a classroom environment /

The introduction of computer and communications technology, and particularly the internet, into education has opened up some new possibilities for teaching and learning. Courses designed and delivered in an online environment offer the possibility of highly interactive and individually focussed teaching and learning experiences. However, online courses also present new challenges for both teachers and students. A qualitative study was conducted to explore teachers' perceptions about the similarities and differences in teaching in the online and face-to-face (F2F) environments. Focus group discussions were held with 5 teachers; 2 teachers were interviewed in depth. The participants, 3 female and 2 male, were full-time teachers from a large College of Applied Arts & Technology in southern Ontario. Each of them had over 10 years of F2F teaching experience and each had been involved in the development and teaching of at least one online course. i - -; The study focussed on how teaching in the online environment compares with teaching in the F2F environment, what roles teachers and students adopt in each setting, what learning communities mean online and F2F and how they are developed, and how institutional policies, procedures, and infrastructure affect teaching and learning F2F and online. This study was emic in nature, that is the teachers' words determine the themes identified throughout the study. The factors identified as affecting teaching in an online environment included teacher issues such as course design, motivation to teach online, teaching style, role, characteristics or skills, and strategies. Student issues as perceived by the teachers included learning styles, role, and characteristics or skills. As well, technology issues such as a reliable infrastructure, clear role and responsibilities for maintaining the infrastructure, support, and multimedia capability affected teaching online. Finally, administrative policies and procedures, including teacher selection and training, registration and scheduling procedures, intellectual property and workload policies, and the development and communication of a comprehensive strategic plan were found to impact on teaching online. The teachers shared some of the benefits they perceived about teaching online as well as some of the challenges they had faced and challenges they perceived students had faced online. Overall, the teachers feh that there were more similarities than differences in teaching between the two environments, with the main differences being the change from F2F verbal interactions involving body language to online written interactions without body language cues, and the fundamental reliance on technology in the online environment. These findings support previous research in online teaching and learning, and add teachers' perspectives on the factors that stay the same and the factors that change when moving from a F2F environment to an online environment.

Moral reasoning and ethics in educational leadership /

School leaders face difficult decisions regarding discipline matters. Often, such decisions play an important role in determining the moral tone of the school and the health of the school community. Many stakeholders are affected by the outcome of such decisions. Codes of conduct, board and school policies, and discipline meetings are often shrouded under secrecy, making the discipline process mysterious. .; In this study I examined the process of moral reasoning. I sought to determine the extent to which school leaders were aware that they were involved in a process of moral reasoning, and ftirthermore, what kind of moral reasoning they practiced. As well, I investigated the ethical grounds and foundations underlying moral reasoning. Thus, in this study I probed the awareness of the process of moral reasoning and sought to find the ethical grounding of decision making. This qualitative study featured short field research. The process involved individual interviews with three different participants: school leaders of a public. Catholic, and an independent school. It found that each school leader practiced moral reasoning to varying degrees through the discipline process. It also explored the possible democratization of moral reasoning by linking to concepts such as fairness, due process, public accountability, and greater participation in the administering of discipline. This study has implications for practice, theory, and future research. The examination of school leaders as the primary focus for discipline matters opens the door to future research that could explore differences between the school systems and possibly other parties affected by moral reasoning in discipline cases.

Teaching media literacy skills about commercials: a comparative analysis of media literacy instruction /

In this study, methods of media literacy instruction including analytic activities, production activities, and a combination of analytic and production activities were compared to determine their influence on grade 8 students' knowledge, attitudes, and behaviours towards commercials. The findings showed that media literacy instruction does improve media literacy skills. Specifically, activities that included an analytic component or an analytic and production component were significantly better than activities that included a production component. Participants that completed analytic or analytic and production activities were able to discern media-related terms, target audience, selling techniques, social values, and stereotypes in commercials better than participants that completed only production activities. The research findings also showed obstacles when teaching media literacy. When engaged in analytic activities, the difficulties included locating suitable resources, addressing the competition from commercials, encouraging written reflection, recognizing social values, and discussing racial stereotypes. When engaged in production activities, the difficulties were positioning recording stations, managing group work, organizing ideas, filming the footage, computer issues, and scheduling time. Strategies to overcome these obstacles are described.

Exploring critical-care nurses' perceptions about critical thinking /

The influx of nurses to the critical-care environment is continuous. In many workplaces, the nurses who are new to critical care are also newly graduated nurses. These new critical-care nurses and their critical-care nursing colleagues, who may have worked in critical care for many years, need to demonstrate expert judgment in order to optimize the potential for positive patient outcomes. The purpose of this study was to explore critical-care nurses' perceptions about critical thinking and expert nursing judgment. Using grounded theory research design, I collected data from 1 1 critical-care nurses through focus groups, an interview, and postparticipation questionnaires. I have articulated a Critical-thinking Modelfor Expert Nursing Judgment. The educational model is directly relevant to practicing critical-care nurses and nursing leaders who guide critical-care nursing practice. The Critical-thinking Modelfor Expert Nursing Judgment contributes to educational theory by objectifying the substantive topic of critical thinking and expert judgment. The model has broad applicability within the domain of education and specific applicability within the domain of nursing education.

Exploring the impact of a hands-on intervention on grade 7 girls and their feelings about self, mathematics, science, technology and related careers

Forty-five 12- and 13-year-old females attending Grade 7 in North York, Ontario were randomly selected from a group of 100 females who had volunteered to participate in a oneday hands-on workshop called It's Your Choice at Seneca College. The goals of this intervention were to broaden the career horizons of these students and to help them realize the need to continue mathematics and science through high school in order to keep occupational options unlimited. The young women were given a pre- and post-attitude survey to provide background information. In the month following participation in the workshop the students were interviewed in small groups (S students per group) to discover their perceptions of the impact of the workshop. The interviews revealed that participants felt that after the workshop their feelings of self-confidence increased, specifically with respect to working with their hands. Participants felt more aware of the usefulness and importance of the study of mathematics, science and technology, They also felt that It's Your Choice increased their interest in careers in these domains and helped them to see that these careers are viable choices for females. The interviews also revealed that many of the participants felt that in this society their roles and their choices were influenced and probably limited by the fact that they are female.

Husserl's approach to transcendental intersubjectivity

It is our intention in the course of the development of this thesis to give an account of how intersubjectivity is "eidetically" constituted by means of the application of the phenomenological reduction to our experience in the context of the thought of Edmund Husserl; contrasted with various representative thinkers in what H. Spiegelberg refers to as "the wider scene" of phenomenology. That is to say, we intend to show those structures of both consciousness and the relation which man has to the world which present themselves as the generic conditions for the possibility of overcoming our "radical sol itude" in order that we may gain access to the mental 1 ife of an Other as other human subject. It is clear that in order for us to give expression to these accounts in a coherent manner, along with their relative merits, it will be necessary to develop the common features of any phenomenological theory of consdousness whatever. Therefore, our preliminary inquiry, subordinate to the larger theme, shall be into some of the epistemological results of the application of the phenomenological method used to develop a transcendental theory of consciousness. Inherent in this will be the deliniation of the exigency for making this an lIintentional ll theory. We will then be able to see how itis possible to overcome transcendentally the Other as an object merely given among other merely given objects, and further, how this other is constituted specifically as other ego. The problem of transcendental intersubjectivity and its constitution in experience can be viewed as one of the most compelling, if not the most polemical of issues in phenomenology. To be sure, right from the beginning we are forced to ask a number of questions regarding Husserl's responses to the problem within the context of the methodological genesis of the Cartesian Meditations, and The Crisis of European Sciences and Transcendental Phenomenology. This we do in order to set the stage for amplification. First, we ask, has Husserl lived up to his goal, in this connexion, of an apodictic result? We recall that in his Logos article of 1911 he adminished that previous philosophy does not have at its disposal a merely incomplete and, in particular instances, imperfect doctrinal system; it simply has none whatever. Each and every question is herein controverted, each position is a matter of individual conviction, of the interpretation given byaschool, of a "point of view". 1. Moreover in the same article he writes that his goal is a philosophical system of doctrine that, after the gigantic preparatory work. of generations, really be- . gins from the ground up with a foundation free from doubt and rises up like any skilful construction, wherein stone is set upon store, each as solid as the other, in accord with directive insights. 2. Reflecting upon the fact that he foresaw "preparatory work of generations", we perhaps should not expect that he would claim that his was the last word on the matter of intersubjectivity. Indeed, with 2. 'Edmund Husserl, lIPhilosophy as a Rigorous Science" in Phenomenology and theCrisis6fPhilosophy, trans". with an introduction by Quentin Lauer (New York.: Harper & Row, 1965) pp. 74 .. 5. 2Ibid . pp. 75 .. 6. 3. the relatively small amount of published material by Husserl on the subject we can assume that he himself was not entirely satisfied with his solution. The second question we have is that if the transcendental reduction is to yield the generic and apodictic structures of the relationship of consciousness to its various possible objects, how far can we extend this particular constitutive synthetic function to intersubjectivity where the objects must of necessity always remain delitescent? To be sure, the type of 'object' here to be considered is unlike any other which might appear in the perceptual field. What kind of indubitable evidence will convince us that the characteristic which we label "alter-ego" and which we attribute to an object which appears to resemble another body which we have never, and can never see the whole of (namely, our own bodies), is nothing more than a cleverly contrived automaton? What;s the nature of this peculiar intentional function which enables us to say "you think just as I do"? If phenomenology is to take such great pains to reduce the takenfor- granted, lived, everyday world to an immanent world of pure presentation, we must ask the mode of presentation for transcendent sub .. jectivities. And in the end, we must ask if Husserl's argument is not reducible to a case (however special) of reasoning by analogy, and if so, tf this type of reasoning is not so removed from that from whtch the analogy is made that it would render all transcendental intersubjective understandtng impos'sible? 2. HistoticalandEidetic Priority: The Necessity of Abstraction 4. The problem is not a simple one. What is being sought are the conditions for the poss ibili:ty of experi encing other subjects. More precisely, the question of the possibility of intersubjectivity is the question of the essence of intersubjectivity. What we are seeking is the absolute route from one solitude to another. Inherent in this programme is the ultimate discovery of the meaning of community. That this route needs be lIabstract" requires some explanation. It requires little explanation that we agree with Husserl in the aim of fixing the goal of philosophy on apodictic, unquestionable results. This means that we seek a philosophical approach which is, though, not necessarily free from assumptions, one which examines and makes explicit all assumptions in a thorough manner. It would be helpful at this point to distinguish between lIeidetic ll priority, and JlhistoricallJpriority in order to shed some light on the value, in this context, of an abstraction.3 It is true that intersubjectivity is mundanely an accomplished fact, there havi.ng been so many mi.llions of years for humans to beIt eve in the exi s tence of one another I s abili ty to think as they do. But what we seek is not to study how this proceeded historically, but 3Cf• Maurice Natanson;·TheJburne in 'Self, a Stud in Philoso h and Social Role (Santa Cruz, U. of California Press, 1970 . rather the logical, nay, "psychological" conditions under which this is possible at all. It is therefore irrelevant to the exigesis of this monograph whether or not anyone should shrug his shoulders and mumble IIwhy worry about it, it is always already engaged". By way of an explanation of the value of logical priority, we can find an analogy in the case of language. Certainly the language 5. in a spoken or written form predates the formulation of the appropriate grammar. However, this grammar has a logical priority insofar as it lays out the conditions from which that language exhibits coherence. The act of formulating the grammar is a case of abstraction. The abstraction towards the discovery of the conditions for the poss; bi 1 ity of any experiencing whatever, for which intersubjective experience is a definite case, manifests itself as a sort of "grammar". This "grammar" is like the basic grammar of a language in the sense that these "rulesil are the ~ priori conditions for the possibility of that experience. There is, we shall say, an "eidetic priority", or a generic condition which is the logical antecedent to the taken-forgranted object of experience. In the case of intersubjectivity we readily grant that one may mundanely be aware of fellow-men as fellowmen, but in order to discover how that awareness is possible it is necessary to abstract from the mundane, believed-in experience. This process of abstraction is the paramount issue; the first step, in the search for an apodictic basis for social relations. How then is this abstraction to be accomplished? What is the nature of an abstraction which would permit us an Archimedean point, absolutely grounded, from which we may proceed? The answer can be discovered in an examination of Descartes in the light of Husserl's criticism. 3. The Impulse for Scientific Philosophy. The Method to which it Gives Rise. 6. Foremost in our inquiry is the discovery of a method appropriate to the discovery of our grounding point. For the purposes of our investigations, i.e., that of attempting to give a phenomenological view of the problem of intersubjectivity, it would appear to be of cardinal importance to trace the attempt of philosophy predating Husserl, particularly in the philosophy of Descartes, at founding a truly IIscientific ll philosophy. Paramount in this connexion would be the impulse in the Modern period, as the result of more or less recent discoveries in the natural sciences, to found philosophy upon scientific and mathematical principles. This impulse was intended to culminate in an all-encompassing knowledge which might extend to every realm of possible thought, viz., the universal science ot IIMathexis Universalis ll •4 This was a central issue for Descartes, whose conception of a universal science would include all the possible sciences of man. This inclination towards a science upon which all other sciences might be based waS not to be belittled by Husserl, who would appropriate 4This term, according to Jacab Klein, was first used by Barocius, the translator of Proclus into Latin, to designate the highest mathematical discipline. . 7. it himself in hopes of establishing, for the very first time, philosophy as a "rigorous science". It bears emphasizing that this in fact was the drive for the hardening of the foundations of philosophy, the link between the philosophical projects of Husserl and those of the philosophers of the modern period. Indeed, Husserl owes Descartes quite a debt for indicating the starting place from which to attempt a radical, presupositionless, and therefore scientific philosophy, in order not to begin philosophy anew, but rather for the first time.5 The aim of philosophy for Husserl is the search for apodictic, radical certitude. However while he attempted to locate in experience the type of necessity which is found in mathematics, he wished this necessity to be a function of our life in the world, as opposed to the definition and postulation of an axiomatic method as might be found in the unexpurgated attempts to found philosophy in Descartes. Beyond the necessity which is involved in experiencing the world, Husserl was searching for the certainty of roots, of the conditi'ons which underl ie experience and render it pOssible. Descartes believed that hi~ MeditatiOns had uncovered an absolute ground for knowledge, one founded upon the ineluctable givenness of thinking which is present even when one doubts thinking. Husserl, in acknowledging this procedure is certainly Cartesian, but moves, despite this debt to Descartes, far beyond Cartesian philosophy i.n his phenomenology (and in many respects, closer to home). 5Cf. Husserl, Philosophy as a Rigorous Science, pp. 74ff. 8 But wherein lies this Cartesian jumping off point by which we may vivify our theme? Descartes, through inner reflection, saw that all of his convictions and beliefs about the world were coloured in one way or another by prejudice: ... at the end I feel constrained to reply that there is nothing in a all that I formerly believed to be true, of which I cannot in some measure doubt, and that not merely through want of thought or through levity, but for reasons which are very powerful and maturely considered; so that henceforth I ought not the less carefully to refrain from giving credence to these opinions than to that which is manifestly false, if I desire to arrive at any certainty (in the sciences). 6 Doubts arise regardless of the nature of belief - one can never completely believe what one believes. Therefore, in order to establish absolutely grounded knowledge, which may serve as the basis fora "universal Science", one must use a method by which one may purge oneself of all doubts and thereby gain some radically indubitable insight into knowledge. Such a method, gescartes found, was that, as indicated above by hi,s own words, of II radical doubt" which "forbids in advance any judgemental use of (previous convictions and) which forbids taking any position with regard to their val idi'ty. ,,7 This is the method of the "sceptical epoche ll , the method of doubting all which had heretofor 6Descartes,Meditations on First Philosophy, first Med., (Libera 1 Arts Press, New York, 1954) trans. by L. LaFl eur. pp. 10. 7Husserl ,CrisiS of Eliroeari SCiences and Trariscendental Phenomenology, (Northwestern U. Press, Evanston, 1 7 ,p. 76. 9. been considered as belonging to the world, including the world itself. What then is left over? Via the process of a thorough and all-inclusive doubting, Descartes discovers that the ego which performs the epoche, or "reduction", is excluded from these things which can be doubted, and, in principle provides something which is beyond doubt. Consequently this ego provides an absolute and apodictic starting point for founding scientific philosophy. By way of this abstention. of bel ief, Desca'rtes managed to reduce the worl d of everyday 1 ife as bel ieved in, to mere 'phenomena', components of the rescogitans:. Thus:, having discovered his Archimedean point, the existence of the ego without question, he proceeds to deduce the 'rest' of the world with the aid of innate ideas and the veracity of God. In both Husserl and Descartes the compelling problem is that of establ ishing a scientific, apodictic phi'losophy based upon presuppos itionless groundwork .. Husserl, in thi.s regard, levels the charge at Descartes that the engagement of his method was not complete, such that hi.S: starting place was not indeed presupositionless, and that the validity of both causality and deductive methods were not called into question i.'n the performance of theepoche. In this way it is easy for an absolute evidence to make sure of the ego as: a first, "absolute, indubitablyexisting tag~end of the worldll , and it is then only a matter of inferring the absolute subs.tance and the other substances which belon.g to the world, along with my own mental substance, using a logically val i d deductive procedure. 8 8Husserl, E.;' Cartesian 'Meditation;, trans. Dorion Cairns (Martinus Nijhoff, The Hague, 1970), p. 24 ff.

Students' knowledge about tobacco one year after receiving the PAL smoking prevention program

A review of literature revealed that the control of cigarette smoking could do more to improve health than any other single action in the field of preventive medicine. In Ontario, since 1989, both Public Health Units and Boards ofEducations have been mandated to provide educational studies related to tobacco use prevention. Even given this fact, there has been an increase in smoking behaviQurs at an earlier age and in females in particular. Smoking prevention progralns must use the most effective means to assist students to obtain the knowledge and skills required to remain or becom'e nonsmokers. In the Niagara Region, PAL smoking prevention programs are offered in some, but not all, schools. As a form of program evaluation, this research sought to determine if students who had PAL could answer correctly a greater number of smoking-related questions than students who did not have this program. Findings reported that students who had PAL in Grade 6 were able to correctly answer more knowledge-based questions (at a statistically significant level), could provide ways to refuse cigarettes at a greater rate, and were able to provide more reasons for remaining nonsmokers. Students who had smoking prevention programming re,ported smoking behavio'urs at a lower rate than those who did not receive this type of program.

Why do some adults change their minds about what is important in the visual arts? : a case study

This-~-case study used ethnographic-methodo-logy. --The research project was an introductory study of one adult's present and past experiences with the visual arts, exploring, in particular, the causes and processes that were related to the individual's changes of mind in order to develop an understanding of why that individual had changed her mind about what was significant in the visual arts. The individual who provided the data was a solid supporter of art galleries: female, middle-aged, graduate of university and college, married with two children, and living in an urban community. The data were collected from two informal conversational interviews and from a written description of one change experience selected by the participant. The individual had positive experiences with art during early childhood, in elementary and secondary school, during university, in avocational drawing and painting studio courses, and in aesthetic experiences. All of these experiences have had individual effects and, together, they have had a cumulative effect on the development of the participant's opinions and ideas about the visual arts. The experiences which had the most effect on the development of the individual's perspectives on the visual arts were handson studio, educational, and aesthetic experiences. Further research is suggested to investigate why some adults change their minds about the visual arts.

Violent Video Game Playing, Moral Reasoning, and Attitudes Towards Violence in Adolescents: Is There a Connection?

In this study of 109 adolescents from the eighth grade of seven public elementary schools in Ontario, the relationship among adolescents’ violent video game playing patterns, habits and attitudes, their levels of moral reasoning, and their attitudes towards violence in real life was investigated. In addition, gender differences were addressed. The mixed-methodology was employed combining qualitative and quantitative data. The research results confirmed that playing video games in general is a very popular activity among those adolescents. Significant negative relationship was found between adolescents’ amount of time playing violent video games during the day and their scores on The Sociomoral Reflection Measure. Significant difference was also found between adolescents who play violent video games and those who do not play violent video games on their scores on The Attitudes Towards Violence Scale. Boys and girls significantly differed in the amount of playing video games during the day, the reasons for playing video games, their favourite video game choices, and their favourite video game character choices. Boys and girls also significantly differed on their choices of personality traits of selected video game characters, the identification with video game characters, and their mood experiences while playing video games. The findings are put into the educational context and the context of normal development, and suggestions are given for parents, for educators, and for future violent video game research.