Specifications are necessary for communicating decisions and intentions and for documenting results at many stages of the program development process. Informal specifications are typically used today, but they are imprecise and often ambiguous. Formal specifications are precise and exact but are more difficult to write and understand. We present work aimed toward enabling the practical use of formal specifications in program development, concentrating on the Clear language for structured algebraic specification. Two different but equivalent denotational semantics for Clear are given. One is a version of a semantics due to Burstall and Goguen with a few corrections, in which the category-theoretic notion of a colimit is used to define Clear's structuring operations independently of the underlying 'institution' (logical formalism). The other semantics defines the same operations by means of straightforward set-theoretic constructions; it is not institutionindependent but it can be modified to handle all institutions of apparent interest. Both versions of the semantics have been implemented. The settheoretic implementation is by far the more useful of the two, and includes a parser and typechecker. An implementation is useful for detecting syntax and type errors in specifications, and can be used as a front end for systems which manipulate specifications. Several large specifications which have been processed by the set-theoretic implementation are presented. A semi-automatic theorem prover for Clear built on top of the Edinburgh LCF system is described. It takes advantage of the structure of Clear specifications to restrict the available information to that which seems relevant to proving the theorem at hand. If the system is unable to prove a theorem automatically the user can attempt the proof interactively using the high-level primitives and inference rules provided. We lay a theoretical foundation for the use of Clear in systematic program development by investigating a new notion of the implementation of a specification by a lower-level specification. This notion extends to handle parameterised specifications. We show that this implementation relation is transitive and commutes with Clear's structuring operations under certain conditions. This means that a large specification can be refined to a program in a gradual and modular fashion, where the correctness of the individual refinements guarantees the correctness of the resulting program.

Not everyone can understand the regular news reports that are broadcast on television. The Swedish public service television company (SVT) therefore produces the newscast News in easy Swedish (Nyheter på lätt svenska), where the language is simplified. The purpose of this thesis is to investigate the comprehensibility of the audiovisual language in News in easy Swedish. Another purpose is to compare the level of comprehension in the audiovisual language in News in easy Swedish with that in SVT's regular newscast Aktuellt and Rapport. The foundation point is what content can be considered understandable for an audience who needs more time and more straightforward information than others in order to understand. The target audience could be, for example, people with cognitive disabilities. No individuals from the target group have been interviewed. Instead, knowledge of what is understandable to them has been obtained from projects where the target group is represented: Inclusion Europe (no date), Comprehensive text (Begriplig text) (2019) and EASIT (2021).  A total of seven news units have been transcribed, analyzed and compared. Five of these come from News in easy Swedish, one from Rapport and one from Aktuellt. The analytical methods utilized have been both quantitative and qualitative. The verbal auditory language has been analyzed using traditional readability methods, such as LIX and nominal ratio. Speech rate has been considered, but not inflection. The exposure time of images has been estimated and the presence of environmental noise has been noted. Subsequently, a qualitative analysis was made of how different semiotic resources interact. Finally, the results from the different news items were compared with each other.  The readability analysis illustrates that in the analyzed material there are no major differences in the level of verbal difficulty between News in easy Swedish, Rapport and Aktuellt. One of the news items on News in easy Swedish has the highest LIX and nominal ratio results, which indicates that it is the most difficult. At the same time, another news item from News in easy Swedish results in the lowest values, indicating that it is the easiest to comprehend.  No example was found in the material regarding how the semiotic resources counteract each other and thus affect information to becoming more difficult to understand. On the other hand, there are examples of news items where an improved collaboration between the semiotic elements could enable enhanced comprehension, for example through a more concise description of what is seen and heard. News in easy Swedish does not have its own film team but reworks material produced for other news programs. The program News in easy Swedish is just under five minutes long and is broadcast five days a week. The lack of own material and the short duration of newscasts are two factors that limit the prospect of creating comprehensible news for an audience who requires more time to be able to understand.