A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKS En el desarrollo formal de software, la especificación formal se utiliza con fines de verificación y validación. Se han definido diferentes tipos de especificaciones formales. En esta tesis nos centraremos en especificaciones algebraicas. Este tipo de especificaciones formales son especificaciones axiomáticas, que suelen definirse en un lenguaje de especificación que incluye diferentes operadores de estructuración. La semántica de estos operadores se define de una forma que sea lo más independiente posible de la lógica de especificación o institución. Otra etapa fundamental en métodos formales es el diseño de software. Las tareas básicas que suelen realizarse durante esta etapa son la deducción de propiedades a partir de una especificación, el refinamiento de especificaciones o verificar que un programa satisface una especificación. Entendemos por entorno de diseño algebraico a un formalismo que incluye la definición de un lenguaje de especificación algebraica con semántica formal y la definición implícita o explícita de, al menos, las dos primeras de las tres tareas de diseño mencionadas anteriormente. Es importante que la definición de los entornos de diseño algebraico sea tambien lo más independiente posible de la lógica del lenguaje de especificación y, si es el caso, que la definición sea para una clase arbitraria de lenguajes de programación. El entorno de diseño algebraico con el que trabajaremos en esta tesis está basado en un lenguaje de especificación muy sencillo que ha sido utilizado para dar semántica a otros lenguajes de especificación de más alto nivel. El principal objetivo de esta tesis es definir un marco formal que permite reusar demostradores de teoremas para teorías de tipos con tipos dependientes e inductivos para el desarrollo de demostradores de teoremas para entornos de diseño algebraico. El problema puede considerarse interesante por varios motivos. Primero, esperamos que el desarrollo de este tipo de herramientas incrementará el uso de este tipo de métodos formales. Segundo, la investigación a realizar es completamente diferente a los trabajos realizados anteriormente y por último, el trabajo requiere un conocimiento extenso de una familia de formalismos no standard que forman las diferentes teorías de tipos con tipos dependientes que se han definido. En esta tesis, primero presentamos de forma general, las características basicas y las aplicaciones de las diferentes teorías de tipos con tipos dependientes. Estudiamos con más detalle la teoría de tipos que vamos a utilizar en el resto de la tesis, y a continuación presentamos un nuevo principio de codificación de sistemas de demostración finitos para la teoría de tipos escogida que mejora algunas de las limitaciones de otros principios de codificación existentes.Con el fin de comparar de forma abstracta las diferentes semánticas dadas a ciertos operadores de comportamiento del lenguaje de especificación escogido, definimos una institución a la que denominamos institución algebraica de comportamiento. Esta institución es también útil para definir las formas normales de las especificaciones que son necesarias para definir cierta clase de sistemas de demostración. A continuación, presentamos diferentes sistemas de demostración para la deducción de propiedades a partir de especificaciones y para el refinamiento de especificaciones. La principal aportación en esta parteconsiste en rediseñar los sistemas de demostración que no es posible dar representaciones adecuadas en la teoría de tipos escogida por ser sistemas de demostración infinitarios.Finalmente, damos una representación en la teoría de tipos de los sistemas de demostración más significativos de nuestro entorno de diseño algebraico usando el nuevo principio de codificación presentado en la tesis. Esto nos permite reutilizar los demostradores de teoremas de la teoría de tipos escogida para el desarrollo de demostradores de teoremas del entorno de diseño algebraico escogido. A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKSIn software engineering, a formal specification of what a system has to do plays a crucial role in the software development process. Formality is required for verification and validation purposes. Different forms of formal specifications have been developed. This thesis concentrates on the algeraic approach to system specification. In essence, this approach can be characterized by:· Axiomatic specifications which consist of a signature together with a set of axioms in a specification logic which any implementation of the system with that specification has to satisfy.· Operations to combine and modify specifications from subspecifications with an algebraic semantics.· An abstract presentation of the semantics as independent as possible of the specification logic or institution.Another crucial step in the software development process is software design. Some of the usual tasks which are performed during software design are the following: deduction of properties from specifications, refinement of specifications and verification of a program with respect to a specification. We understand by an algebraic design framework a formalism which includes a formal definition of an algebraic specification language including a model-theoretic semantics and the implicit or explicit formal definition of at least the two first software design tasks. The definition of algebraic design frameworks should be for several specification logics or even better for an arbitrary but fixed institution, and if it is the case for an arbitrary class of programming languages. In the literature, there exists a large amount of algebraic specification languages and algebraic design frameworks. The algebraic design framework which we will work in this thesis will be based on a kernel and simple algebraic specification language. The main objective of this thesis is to give an approach to reuse theorem provers for type theories with dependent and inductive types for the development of theorem provers for algebraic design frameworks. The problem can be considered interesting for several reasons. First, we believe that the development of tools in type-theoretic theorem provers will help to spread the use of algebraic techniques. Note that these kind of theorem provers have been widely used and applied. Second, the work to be done is completely different to the work done before and finally this work requires a thorough understanding of a non-standard family of formalisms which are type theories. In this thesis, first we give an overall view of type theories together with their apllications and then we present a new principle of encoding in an expressive type theory which solves some of the limitations of previous principle of encodings. In order to give a generic presentation of the framework of ASL for different specification logics, we give an abstract semantic framework in which the semantics of the the behavioural operators of ASL can be uniformly instantiated in first-order and higher-order logic. We also redesign the different proof systems for deduction and refinement when it is not possible to give adequate encodings in the type theory because they are infinatary proof systems. In some cases, different solutions are given for first and higher-order logics. Finally, the main proof systems of the algebraic design framework for ASL have been encoded in UTT using the new principle of encoding presented in the thesis. This allows us to take advantage of the current implementation of theorem provers for UTT to implement proof checkers for the proof systems of our chosen algebraic design framework.

Definimos el objeto de estudio, focalizado, entorno al complejo entramado que configura el problema idea de idea de proyecto de obra como ¿objeto de saber¿ en relación al proyecto artístico. A través de la revisión y el cuestionamiento de la relación práctica artística y universidad, proponemos una metodología denominada elementos discursivos, creando para ello un marco didáctico que recoge la experiencia, el proceso de reflexión y la puesta en práctica tanto en el contexto de la producción artística, la crítica o la docencia. Si consideramos que ¿la enseñanza del arte es una parte importante de la producción de arte¿, la formación del artista en la universidad del siglo XXI cobra un lugar relevante sobre las cuestiones que deberíamos problematizar: por ejemplo, ¿qué modelos pedagógicosse utilizan considerando que ¿el arte es, de hecho, la definición del arte¿, y qué es, o no, relevante en estos modelos?, ¿el aprendizaje de contenidos o el desarrollo de destrezas cognitivas mediante métodos? ¿Desde los estudios de arte se piensa la idea de universidad, la pertenencia al ámbito de las humanidades? ¿En virtud de qué construimos una obra de arte? o ¿cómo es que se piensa la idea de una obra de arte? De partida, estas preguntas iniciales parecen no ser suficientes al presuponer otras aún más amplias que las abarcan y que en su extensión tratan sobre significados filosóficos, estudios pedagógicos, sociológicos o históricos. Pensamos, sin embargo, que desde nuestra área de conocimiento deberíamos reflexionar sobre los procesos formativos del arte, señalando la necesidad de adquirir ¿como argumentaba José Luis Brea¿ ¿herramientas conceptuales que proporcionen un conocimiento crítico del mundo contemporáneo¿ y sobre la situación problemática del conocimiento crítico del mundo y por extensión, de las contribuciones del conocimiento artístico a este conocimiento crítico. Por ello llevamos a cabo esta investigación sobre procesos formativos del arte contemporáneo en el contexto universitario, con el objetivo de reflexionar sobre las posibilidades de un principio de análisis crítico-disciplinar (de base metodológica), que podría objetivar, conceptual y críticamente, los procesos formativos de la idea de idea de proyecto de obra en relación al proyecto artístico. Esta metodología didáctica que nombramos ¿elementos discursivos: el problema de la idea de idea de proyecto de obra como ¿objeto de saber¿ en relación al proyecto artístico¿, concentra (o debería concentrar) algo que de hecho es aún más complejo: ideas, imágenes, hechos y datos de la comprensión del propio elemento (el sujeto), imágenes del pensamiento en las que el artista proyecta su concepción de sí mismo (mundos de vida), y que constituye, en la medida en que organiza su experiencia y, por lo mismo, punto de vista y perspectiva sobre el conocimiento del mundo (realidades del saber). Entendemos la metodología didáctica de los elementos discursivos como una relación, como un anclaje entre partes cooperantes equilibradas de significación, de ámbitos_sistemas, de producción de criticidad. Aunque podemos hablar de ¿elementos discursivos¿ como si fuesen entidades separadas, existen solamente en cuanto componentes_colaborantes de la idea de obra en relación al conocimiento crítico del mundo: por un lado, como inductores potenciales de las funciones semánticas, por otro lado, como referencias exteriores de la mismidad de la cosa idea, y por otro, como subtextos de supuestos implícitos ¿de proposiciones¿ sobre la naturaleza de las realidades de saber que la envuelve, o, de la entonces posible realidad de acogida en tanto que operación constructiva transformada en ¿hecho¿. Hablamos, por tanto, de una metodología didáctica que piensa la idea de idea de proyecto de obra, de un pensamiento que haría permisible dar mención ¿bajo el supuesto de una conciencia de la experiencia de obra¿ a la procesualidad en tanto que forma, también, de producción de conocimiento. Todo esfuerzo por la consolidación de una metodología didáctica de las artes debería concentrar su atención en todo aquello concerniente, y que se da, en la experiencia de la visualidad (¿el arte trabaja con ideas plasmadas en un orden de visualidad¿), pero también, en las relaciones y flujos de conexión que tienen lugar con los otros órdenes de la experiencia, en la telaraña de su condicionalidad ¿de la explicación ordenada de las radiaciones que la constituyen y materializan. / Miyares Puig, BJ. (2013). ELEMENTOS DISCURSIVOS: El problema de la idea de idea de proyecto de obra como "objeto de saber" en relación al proyecto artístico [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/31635 / TESIS

L'objectiu principal d'aquesta tesi és millorar l'actual capacitat de predicció de fenòmens meteorològics de pluja intensa potencialment perillosos a la Mediterrània occidental. Es desenvolupen i verifiquen tres sistemes de predicció per conjunts (SPC) que tenen en compte incerteses presents en els models numèrics i en les condicions inicials. Per generar els SPC s'utilitza la connexió entre les estructures de vorticitat potencial (VP) i els ciclons, a més de diferents esquemes de parametrització física. Es mostra que els SPC proporcionen una predicció més hàbil que la determinista. Els SPC generats pertorbant les condicions inicials han obtingut millor puntuació en verificacions estadístiques. Els resultats d'aquesta tesi mostren la utilitat i la idoneïtat dels mètodes de predicció basats en la pertorbació d'estructures de VP de nivells alts, precursors de les situacions ciclòniques. Els resultats i estratègies presentats pretenen ser un punt de partida per a futurs estudis que facin ús d'aquests mètodes. / The main goal of this thesis is to improve the current prediction skill of potentially hazardous heavy precipitation weather events in the western Mediterranean region. We develop and test three different ensemble prediction systems (EPSs) that account for uncertainties present in both the numerical models and the initial conditions. To generate the EPSs we take advantage of the connection between potential vorticity (PV) structures and cyclones, and use different physical parameterization schemes. We obtain an improvement in forecast skill when using an EPS compared to a determinist forecast. The EPSs generated perturbing the initial conditions perform better in the statistical verification scores. The results of this Thesis show the utility and suitability of forecasting methods based on perturbing the upper-level precursor PV structures present in cyclonic situations. The results and strategies here discussed aim to be a basis for future studies making use of these methods.

Els mètodes de verificació formal s'estan usant cada vegada més en la indústria per establir la correctessa i trobar els errors en models de sistemes; per exemple la descripció de hardware, protocols, programes distribuïts, etc. En particular, els verificadors de models ho fan automàticament per sistemes d'estats finits, per-o estan limitats degut al problema de l'explosió d'estats; i la verificació formal interactiva, l'àrea d'aquesta tesi, es necessita.L'enfocament de la verificació automàtica treballa sobre el sistema de transicions del model, el qual defineix la seva semàntica. Aquest sistema de transicions té sovint molts estats, i sempre una mida gran comparada amb la mida del model del sistema, el qual és sempre infinit. Aquestes consideracions suggereixen un enfocament de verificació estàtica com els d'aquesta tesi, evitant els sistemes de transicions, treballant directament sobre el model del sistema, en principi, la complexitat computacional hauria de ser menor. L'enfocament estàtic d'aquest treball es fa sobre models de sistemes expressats en notació imperativa amb paral·lelisme explícit, sentències de comunicacions síncrones i variables d'emmagatzematge locals.Els raonaments d'equivalència són molt empleats per números, matrius i altres camps. Tanmateix, per programes imperatius amb paral·lelisme, comunicacions i variables, encara que potencialment sigui un mètode de verificació molt intuïtiu, no han estat massa explorats. La seqüencialització formal via l'eliminació de comunicacions internes, l'àrea d'aquesta tesi, és una demostració basada en el raonament estàtic d'equivalències que, donat que disminueix la magnitud del vector d'estats, pot complementar altres mètodes de demostració. Es basa en l'aplicació d'un conjunt de lleis , apropiades per tal propòsit, com reduccions de reescriptura del model del sistema. Aquestes depenen de la noció d'equivalència i de les suposicions de justícia.Aquesta tesi contribueix a la quasi inexplorada àrea de l'eliminació de comunicacions formal i seqüencialització de models de sistema. Les lleis estan definides sobre una equivalència feble: equivalència d'interfície. L'eliminació de comunicacions est-a limitada a models sense seleccions, per exemple models en els quals les comunicacions internes no estan dins de l'àmbit de sentències de selecció. Aplicacions interessants existeixen dins d'aquest marc. Les lleis són vàlides només per justícia feble o sense justícia. Aquesta ha estat desenvolupada seguint la semàntica proposada per Manna i Pnueli per a sistemes reactius [MP91, MP95]. S'han formulat les condicions d'aplicabilitat per les lleis de la pròpia eliminació de comunicacions. A més a més, es proposa un procediment de construcció de demostracions per l'eliminació de comunicacions, el qual intenta aplicar automàticament les lleis de la eliminació. També s'ha dissenyat un conjunt de procediments de transformació, els quals garanteixen que la transformació equivalent sempre correspon a l'aplicació d'una seqüència de lleis. Degut a que la construcció de les demostracions és impracticable, normalment impossible, sense l'ajuda d'una eina, s'ha desenvolupat un demostrador interactiu per la construcció semiautomàtica de la seqüencialització de models de sistemes i demostracions d'eliminació. Tant els procediments de transformació com els de l'eliminació de comunicacions estan integrats en l'eina. Amb l'ajuda del demostrador s'ha construït la demostració de seqüencialització d'un model, no trivial, de processador pipeline. Per aquest exemple s'ha assolit una reducció, respecte del model original, de la cota superior del nombre d'estats de 2−672.Malgrat l'enorme quantitat d'esforç dedicat a l'àrea, abans i durant la tesi, encara queda molt treball per a que l'eliminació de comunicacions i la seqüencialització sigui realment un mètode pràctic. No obstant els resultats d'aquesta tesi han establert els fonaments i han donat l'estímul necessari per continuar l'esforç. / Los métodos de verificación formal se están usando cada vez más en la industria para establecer la corrección y encontrar los errores en modelos de sistemas; por ejemplo, la descripción de hardware, protocolos, programas distribuidos, etc. En particular, los verificadores de modelos lo hacen automáticamente para sistemas de estados finitos, pero están limitados debido al problema de la explosión de estados; y la verificación formal interactiva, el área de esta tesis, es necesaria.El enfoque de la verificación automática trabaja sobre el sistema de transiciones del modelo, el cual define su semántica. Este sistema de transiciones tiene a menudo muchos estados, y siempre un tamaño grande comparado con el tamaño del modelo del sistema, el cual es siempre infinito. Estas consideraciones sugieren un enfoque de verificación estática como los de esta tesis, evitando los sistemas de transiciones, trabajando directamente sobre el modelo del sistema, en principio, la complejidad computacional tendría que ser menor. El enfoque estático de este trabajo se lleva a cabo sobre modelos de sistemas expresados en notación imperativa con paralelismo explícito, sentencias de comunicaciones síncronas y variables de almacenamiento locales.Los razonamientos de equivalencia son muy empleados para números, matrices y otros campos. Sin embargo, para programas imperativos con paralelismo, comunicaciones y variables, aún teniendo la potencialidad de ser un método de verificación muy intuitivo, no han sido muy explorados. La secuencialización formal vía la eliminación de comunicaciones internas, el área de esta tesis, es una demostración basada en el razonamiento estático de equivalencias que, ya que disminuye la magnitud del vector de estados, puede complementar otros métodos de demostración. Se basa en la aplicación de un conjunto de leyes, apropiadas para tal propósito, como reducciones de reescritura del modelo del sistema. Éstas dependen de la noción de equivalencia y de las suposiciones de justicia.Esta tesis contribuye a la casi inexplorada área de la eliminación de comunicaciones formal y secuencialización de modelos de sistema. Las leyes están definidas sobre una equivalencia débil: equivalencia de interfaz. La eliminación de comunicaciones está limitada a modelos sin selecciones, por ejemplo modelos en los cuales las comunicaciones internas no están dentro del ámbito de sentencias de selección. Aplicaciones interesantes existen dentro de este marco. Las leyes son válidas sólo para justicia débil o sin justicia. Ésta ha sido desarrollada siguiendo la semántica propuesta por Manna y Pnueli para sistemas reactivos [MP91, MP95]. Se han formulado las condiciones de aplicabilidad para las leyes de la propia eliminación de comunicaciones. Además, se propone un procedimiento de construcción de demostraciones para la eliminación de comunicaciones, el cual intenta aplicar automáticamente las leyes de la eliminación. También se ha diseñado un conjunto de procedimientos de transformación, los cuales garantizan que la transformación equivalente siempre corresponde a la aplicación de una secuencia de leyes. Debido a que la construcción de las demostraciones es impracticable, normalmente imposible, sin la ayuda de una herramienta, se ha desarrollado un demostrador interactivo para la construcción semiautomática de la secuencialización de modelos de sistemas y demostraciones de eliminación. Tanto los procedimientos de transformación como los de la eliminación de comunicaciones están integrados en la herramienta. Con la ayuda del demostrador se ha construido la demostración de secuencialización de un modelo, no trivial, de procesador pipeline. Para este ejemplo se ha logrado una reducción, respecto del modelo original, de la cota superior del número de estados de 2−672.A pesar de la enorme cantidad de esfuerzo dedicado al área, antes y durante esta tesis, todavía queda mucho trabajo para que la eliminación de comunicaciones y la secuencialización sea realmente un método práctico. Sin embargo los resultados de esta tesis han establecido los cimientos y han dado el estímulo necesario para continuar el esfuerzo. / Formal verification methods are increasingly being used in industry to establish the correctness of, and to find the flaws in, system models; for instance, descriptions of hardware, protocols, distributed programs, etc. In particular, model checking does that automatically for finite-state systems, but it is limited in scope due to the state explosion problem; and interactive formal verification, the broad area of this thesis, is needed.Automatic verification approaches work on the transition system of the model, which defines its semantics. This transition system has often infinitely many states, and always a large size compared to the size of the system model, which is always finite. These considerations suggest that static verification approaches such as those of this thesis, avoiding the transition system, working directly on the system model would have less computational complexity, in principle. The static approach of this work is carried out on system models expressed in imperative notations with explicit parallelism and synchronous communication statements, and with local storage variables.Equivalence reasoning is heavily used for numbers, matrices, and other fields. However, for imperative programs with parallelism, communications, and variables, although having the potentiality of being a very intuitive verification method, it has not been much explored. Formal sequentialization via internal communication elimination, the area of this thesis, is a static equivalence reasoning proof that, since it decreases the size of the state vector, could complement other proof methods. It is based on the application of a set of laws, suitable for that purpose, as rewriting reductions to a system model. These proofs need both proper communication elimination laws and auxiliary basic laws. These depend on the notion of equivalence and on the fairness assumptions.This thesis contributes to the almost unexplored area of formal communication elimination and system model sequentialization. The laws are defined over a weak equivalence: interface equivalence. Communication elimination is confined to selection-free models, i.e. models none of whose inner communications are within the scope of selection statements. Interesting applications already exist within this framework. The laws are valid only with weak fairness or no fairness. It has been developed following the same semantics as Manna and Pnueli for reactive systems [MP91, MP95]. Applicability conditions for the proper communication elimination laws are derived. In addition, a communication elimination proof construction procedure, which attempts to apply the elimination laws automatically is proposed. A set of transformation procedures, guaranteeing that the equivalence transformation always corresponds to the application of a sequence of laws have been designed as well. Since the construction of elimination proofs is impractical, even impossible, without a tool, an interactive prover for semi-automatic construction of system model sequentialization and elimination proofs has been developed. Both transformation and communication elimination procedures are integrated within the tool. As a non-trivial example, a sequentialization proof of a pipelined processor model, has been constructed with the help of the prover. Areduction, with respect to the original model, of 2−672 on the upper bound on the number of states has been achieved in this example.In spite of the huge amount of effort already devoted to the area, before and during this thesis, much work still needs to be done until communication elimination and sequentialization become a practical method. Nevertheless the results of this thesis have established its foundations and given the necessary encouragement for continuing the effort.