( en | de | ru )

 

  2. тэг
  3. obj3

закладки  8

  •  

    Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification influenced by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation. Rewriting logic is a logic of concurrent change that can naturally deal with state. It has good properties as a general semantic framework for giving executable semantics to a wide range of languages and models of concurrency. In particular, it supports very well concurrent object-oriented computation. The same reasons making rewriting logic a good semantic framework make it also a good logical framework, that is, a metalogic Maude supports in a systematic and efficient way logical reflection; supports an extensible algebra of module composition operations, and allows many advanced metaprogramming and metalanguage apps
    14 лет назад , @draganigajic
     
      csobj3plresearch
      (0)
      копироватьудалить
       
       
    •  

      "OBJ" refers to the language family, with OBJ3, CafeOBJ, BOBJ. The OBJ are algebraic prog and spec languages, based on order sorted equational logic, possibly enriched with other logics (such as rewriting logic, hidden equational logic, or first order logic), with module system of parameterized programming They are logical languages, in the sense that their programs are sets of sentences in some logical system, and their operational semantics is given by deduction in that logical system. All recent OBJ languages use order sorted algebra, with a rigorous basis for user definable sub-types, multiple inheritance, overloading, multiple representations, coercions, etc. also user definable mixfix syntax, execution strategies, and memoization. All recent OBJ languages provide parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse The module systems of Ada, ML, C++ have all been influenced by the OBJ
      14 лет назад , @draganigajic
       
        cslogicobj3plresearch
        (0)
        копироватьудалить
         
         
      •  

        As you probably can tell Maude sets out to solve a different set of problems than ordinary imperative languages. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. Maude lets us define formally what we mean by some concept in a very abstract manner, but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). This is useful to validate security protocols and critical code. The Maude system has proved flaws in cryptography protocols by just specifying what the system can do , and by looking for unwanted situations the protocol can be showed to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do. We can use Maude's built-in search to look for unwanted states, or it can be used to show that no such states can be reached.
        14 лет назад , @draganigajic
         
          logicmaudemetaprogrammingobj3plresearchrewritingwikipedia
          (0)
          копироватьудалить
           
           
        •  

          Sorts are used: * some are used for data values as in the algebraic approach to data types; and * others are used for states, as in the algebraic approach to abstract machines. The latter give objects. These two uses for sorts are dual: induction is used to establish properties of data types; while coinduction is used to establish (behavioral) properties of objects with states. Similarly, initiality is important for data types, while finality is important for states. However, we do not insist that implementations of abstract machines (or objects) must be final Because we use hidden sorts to specify classes of objects, order sorted algebra provides a very natural way to handle inheritance; it also allows specifying partial recursive functions, partially defined functions, subtypes of various kinds, error definition and recovery, coercions and multiple representations. The module system of parameterized programming gives us other forms of inheritance
          14 лет назад , @draganigajic
           
            goguenobj3
            (0)
            копироватьудалить
             
             
          •  

            Algebraic techniques have been very successful in specifying and reasoning about data types. Hidden algebra extends these techniques to systems with state. The hidden algebra approach takes as basic the notion of behavioural abstraction: this means that specifications characterise how objects (and systems) behave. Models of hidden specifications can be thought of as abstract machines that implement the specified behaviour. Behavioural satisfaction of equations means that the left and right sides of the equations denote states that cannot be distinguished by their outputs. In this sense, hidden algebra is an algebraic treatment of abstract automata. * visible sorts are used for data values, while * hidden sorts are used for states. In a sense, these two uses of sorts are dual: induction can be used to establish properties of data types, whereas coinduction establishes properties of objects with state.
            14 лет назад , @draganigajic
             
              csgoguenhiddenAlgebraobj3research
              (0)
              копироватьудалить
               
               

            публикации  

              Нет подходящих.
            • ⟨⟨
            • ⟨
            • ⟩
            • ⟩⟩