De sensibus externis

Arkit: A-B4 C2.

De sangvisuga

Invocatio: KREIKKAA Alpha & omega.

Lekfullhet, ritualer och bundenhet dryftades i Åbo : : den stora valfriheten? : lekfullhet och kontroll : seminarium i folkloristik och religionsvetenskap 5.-6.11.2007 Åbo

Ajankohtaista

Tillbakablickar på religionsvetenskapens utveckling vid Åbo Akademi och utmaningar inom ämnet i dag

Kolumnen

Sorg och drömmar - nostalgi och tystnad : : surusta haaveisiin - nostalgiasta hiljentymiseen : Emotioner och narrativer 11-12.8.2008, Åbo

Aktuellt/Ajankohtaista

Karelsk folklore : kurs och exkursion Folklorister från Åbo besöker Joensuu

Aktuellt

Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Det osynligas arkitektur : om rumsligheten i Bo Carpelans författarskap

Bo Carpelan (f. 1926) har kallats ”rummets diktare” och ”drömarkitekt”. I Carpelans författarskap hittar man formuleringar som ”Det är inte tiden som förändrar oss, det är rummet”, ”Rum bygger upp en startpunkt i hjärtat och tanken, samtidigt.” och ”Rum är levande när människor finns där, men när de dör, upphör rummen.” Avhandlingen är en studie i den rumsliga betoningen i Carpelans författarskap. I en kontext av centrala litteratur- och idéhistoriska strömningar och influenser från bl.a. flamländskt interiörmåleri, uppstår hos Carpelan med tiden en utpräglat rumslig diktkonst och livsåskådning. I ljuset av rumsligheten i Carpelans författarskap framstår verkligheten som ett slags hemlighetsfull skrift som människan kan lära sig läsa men som aldrig helt låter sig tydas.

Repression och legitimering - rysk maktutövning i Åbo generalguvernement 1717-1721 : civilförvaltningen under en ockupation med jämförande utblickar

I avhandlingen undersöks den ryska maktutövningen under stora ofredens civilförvaltningsskede (1717-1721). Var ockupanterna villiga att axla rollen som "god överhet" eller pågick förtrycket oförminskat som under den föregående militära styrelseperioden? Hierarkins och förvaltningens uppbyggnad liksom interaktionen inom den politiska kulturen undersöks. Tjänstemännens förutsättningar att sköta sina uppdrag och deras uppträdande granskas. Slutligen görs en jämförelse med andra ockupationer för att fastställa hur allmängiltiga förhållandena var i Finland under den ryska civilförvaltningsperioden 1717-1721.

Rummet i vårdandets värld

This study is made in the context of basic research within the field ofcaring science. The aim is to make a theoretical and ontological investigation of what the space is in the world of caring. The basic proposition is that the space, as a fundamental dimension, has an impact on how the appreciation of one's mental health and suffering is shaped, and vice versa. The overall purpose is to develop a theoretical model of space from the caring science point of view andalso to offer an ideal concept of space to caring science. Guided by a theoretical horizon (Eriksson 1993, Eriksson 1995, Eriksson 2001) and methodological approach grounded in Gadamer's philosophic and existential hermeneutics a three-stage analysis and interpretation is conducted. The hermeneutic spiral of this investigation starts through a procedure in accordance with Eriksson's model (1997) of concept definition. The goal is to clarify the etymology of the concept as well as semantic differences between synonymous concepts, i.e. to identify the different extents of the concept of `space` (`rum`) in order to bring these closer for an exploration. The second phase is to analyse and interpret a sample of narratives in order to explicate the ontological nature and meaning of the space. The material used here is literary texts. The goal is to clarify the characteristics of the very inside of the space when it is shaped in relation to the human being in encountering suffering. In the third phase an interview study is taken place. The focus of the study is directed towards the phenomenon of space as it is known by a patient in a landscape of psychiatric care, i.e. what the space is in a contextual meaning. Then, a gradual hermeneutic understanding of the space is attempted by using theories from the field of caring science as well as additional theories from other disciplines. Metaphors are used as they are vivid and expressive tools for generating meaning. Different metaphoric space formations depict here a variety of purports that, although not quite the same, share extensive elements. Six metaphorically summarized entities of meaning emerged. The comprehensive form of space is pointed out as the Mobile-Immobile Room. Furthermore, the Standby, the Asylum, the Wall and the Place. In the further dialogue with the texts the understanding has deepened ontologically. The theoretical model ofthe space sums up the vertical, horizontal and the inward extent of deepness inthe movement of mental health. Three entities of ontological meaning have emerged as three significant rooms: the Common Land emerges as the ideal concept of mutual creation in the freedom of doing, being and becoming health. On the interpersonal level it means freedom, which includes sovereignty, choice and dignity of the human being. The Ice World signifies, ultimately, the space as a kind of frozenness of despair which "wallpapers" the person's entire being in the world in the drama of suffering. The Spiritual Home is shaped when the human being has acquired the very core of his/her inner and outer placeness as a kind of "at-homeness" and rootedness. Time is a central element and the inward extent of deepness of this trialectic space. Each of the metaphors is then the human being's unique, although even paradoxical, way of conceiving reality, and mastering spiritual suffering. They condense characteristic structures and patterns of dynamic scenery, which take place within the movement of health. The space encloses a contradictory spatiality constituted through the dynamic field of meaningfulness and meaninglessness. Anyway, it is not through a purging of these contradictions but through bringing them together in a drama of suffering that the space is shaped as ontologically good and meaningful in the world of caring.

Hjärtats vanor, tankens välvilja och handens gärning : dygd som vårdetiskt grundbegrepp

The main aim of the study is to elucidate the meaning and dimensions of the concept of „virtue‟, and to find the place of virtue in a caritative caring ethics, i.e. a caring ethics based on human love and mercy. The intention is to create a theory model which utilizes the possibilities of virtue in developing the caritative caring ethics as a whole. The caritative caring ethics has a universal potential – it is primarily not a professional ethics, but it may form a frame of reference and basis for formulating ethical codes, and for ethical discussions within different caring contexts. The hermeneutic approach of the study is inspired by Gadamer‟s philosophical hermeneutics combined with the view of hermeneutics as a hypothetical-deductive process. The study is guided by Eriksson‟s model of definition of concepts. The concept of „virtue‟ is studied focusing on its ethical dimensions. These ethical dimensions of virtue are seen as anchored to an inner ethos, whereas ethos stands for the ontological goodness, a basic notion of the Good that permeates the entity of the human being, and forms the base of the culture where he lives and acts. The overarching research questions are: 1. What is virtue? 2. What is „virtue‟ as a basic concept in caring science? 3. What place does virtue have in caritative caring ethics? The answer of the first question is mainly searched for by an ontological determination comprising partly an etymologic and semantic analysis of „virtue‟, and partly a determination of the essence of virtue. The answer to the second and third questions are mainly searched for using a contextual determination, where the purposive context and pragmatic features of virtue are studied in relation to caring ethics. The ontological and contextual determinations are brought together through hermeneutical interpretation, forming a new whole, which constitutes the results of the study. The results of the study are depicted in a theory model, in which the movement of virtue from ethos to deed is moulded as caritative caring ethics. The material of the study consists of dictionaries, texts written by Aristotle and St. Thomas Aquinas, articles, dissertations, and books, as well as parts of a pilot survey answered by 33 nurses. The results of the study show that the essence of virtue is primarily functional, not ethical. The ethical emerges when virtue is contextualized in a human communion. Virtue makes something fulfil its function well; makes the human being good, and gives him morals and morality. The human being needs prudence, love, and humility to acquire and develop the moral virtues. Virtue is a power, related to a value, which considering a caritative caring ethics consists of the caritas motif. Human love is shown through deeds, making the human being do what he is expected to do. Virtue, as an active power of becoming, affirms and clarifies the human being‟s ability to develop in the direction of the Good. Virtue becomes essential and unifying when morality appears in the human mind as auctoritas, an inner, prompting power based on divinity or a transcendental ethos. Together ethos and virtue create opportunities for an inner ethics based on voluntariness and joy in being and doing the true, the good, and the beautiful.