ogma-spec (empty) → 1.2.0

raw patch · 5 files changed

+150/−0 lines, 5 filesdep +basesetup-changedbinary-added

Dependencies added: base

Files

• CHANGELOG.md +6/−0
• LICENSE.pdf binary
• Setup.hs +2/−0
• ogma-spec.cabal +75/−0
• src/Data/OgmaSpec.hs +67/−0

@@ -0,0 +1,6 @@+# Revision history for ogma-spec++## [1.2.0] - 2024-01-21++* Version bump 1.2.0 (#117).+* Initial release (#115).

binary file changed (absent → 117991 bytes)

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,75 @@+-- Copyright 2024 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS."
+--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.++cabal-version:       2.0+build-type:          Simple++name:                ogma-spec+version:             1.2.0+homepage:            http://nasa.gov+license:             OtherLicense+license-file:        LICENSE.pdf+author:              Ivan Perez, Alwyn Goodloe+maintainer:          ivan.perezdominguez@nasa.gov+category:            Aerospace+extra-source-files:  CHANGELOG.md++synopsis:            Ogma: Runtime Monitor translator: JSON Frontend++description:         Ogma is a tool to facilitate the integration of safe runtime monitors into+                     other systems. Ogma extends+                     <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime+                     verification framework that generates hard real-time C99 code.+                     .+                     This library contains an abstract representation of an Ogma specification.++-- Ogma packages should be uncurated so that only the official maintainers make+-- changes.+--+-- Because this is a NASA project, we want to make sure that users obtain+-- exactly what we publish, unmodified by anyone external to our project.+x-curation: uncurated++library++  exposed-modules:+    Data.OgmaSpec++  build-depends:+      base >= 4.11.0.0 && < 5++  hs-source-dirs:+    src++  default-language:+    Haskell2010++  ghc-options:+    -Wall

@@ -0,0 +1,67 @@+-- Copyright 2024 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS."+--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.+--+-- | Abstract representation of an Ogma specification.+module Data.OgmaSpec where++-- | Abstract representation of an Ogma specification.+data Spec a = Spec+    { internalVariables :: [ InternalVariableDef ]+    , externalVariables :: [ ExternalVariableDef ]+    , requirements      :: [ Requirement a ]+    }+  deriving (Show)++-- | Internal variable definition, with a given name, its type and definining+-- expression.+data InternalVariableDef = InternalVariableDef+    { internalVariableName    :: String+    , internalVariableType    :: String+    , internalVariableExpr    :: String+    }+  deriving (Show)++-- | External variable definition, with a given name and type.+--+-- The value of external variables is assigned outside Copilot, so they have no+-- defining expression in this type.+data ExternalVariableDef = ExternalVariableDef+    { externalVariableName :: String+    , externalVariableType :: String+    }+  deriving (Show)++-- | Requirement with a given name and a boolean expression.+data Requirement a = Requirement+    { requirementName        :: String+    , requirementExpr        :: a+    , requirementDescription :: String+    }+  deriving (Show)