diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,6 @@ +# Revision history for ogma-spec + +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Initial release (#115). diff --git a/LICENSE.pdf b/LICENSE.pdf new file mode 100644 Binary files /dev/null and b/LICENSE.pdf differ diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ogma-spec.cabal b/ogma-spec.cabal new file mode 100644 --- /dev/null +++ b/ogma-spec.cabal @@ -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 + , 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 diff --git a/src/Data/OgmaSpec.hs b/src/Data/OgmaSpec.hs new file mode 100644 --- /dev/null +++ b/src/Data/OgmaSpec.hs @@ -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)