Skip to content

Latest commit

 

History

6 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

specc-demo

Example project for SpecCompiler — a typed, compiled specification authored in CommonSpec (a small convention layer over CommonMark).

This is the running example of the SpecCompiler dissertation: the specification of a digital-clock firmware, compiled with the sw_docs model.

Click Use this template above to scaffold your own SpecCompiler project from this layout.

Source files:

  • srs.md — requirements (AL-001, TM-001, DP-001) and the data dictionary, referenced inline via [dic:...](#).
  • sdd.md — design (AL-004, TM-004), software units (AL-005, TM-005) and the code symbols they implement.
  • svc.md — verification cases with input/procedure/expected and the auto-generated traceability matrix (traceability_matrix:).
  • tr.md — test results (Pass/Fail); in a real pipeline these objects are generated from JUnit XML reports.
  • symbols.mdgenerated, do not edit: SYMBOL objects extracted from the firmware C sources by scripts/extract_symbols.py (libclang), including the calls: graph used for impact analysis.
  • firmware/ — the digital-clock C sources the specification describes (alarm.c, time_manager.c, ...), with the compile_commands.json used by the symbol extractor. The CSU objects in sdd.md point at these files via file_path.

Build:

specc build project.yaml

Regenerate symbols (requires python3-clang):

python3 scripts/extract_symbols.py firmware symbols.md

Identifiers use a module + sequence scheme (AL-001) instead of embedding the object type: the type comes from the CommonSpec annotation (## HLR: ... @AL-001), not from the identifier.

About

No description, website, or topics provided.

Resources

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages