You’re almost certainly thinking of VDM — the Vienna Development Method — and, more specifically, the VDM specification notation used inside IBM in that period (often called Meta‑IV at the time, later standardized as VDM‑SL).
Why this matches your recollection
- Origin in IBM: VDM grew out of work at IBM’s Vienna Laboratory in the 1970s (initially “Vienna Definition Language” for formally defining PL/I), and by the 1980s IBM groups were using the associated specification notation for software specs.
- Set theory and logic with strong typing: VDM’s notation is explicitly set/logic based, with rich types (sets, sequences, maps, product types, invariants, etc.) and static type checking.
- Tool support: there were type/specification checkers for Meta‑IV/VDM within IBM and, shortly after, external tools appeared (e.g., the IFAD VDM‑SL Toolbox). Many people remember these simply as “the spec checker.”
- Relationship to Z: VDM is somewhat more “programmerly/pragmatic” than Z (Z’s notation is more purely mathematical). Many UK groups (including at IBM Hursley) explored or moved to Z in the later 1980s, which fits your timeline.
What happened to it
- Standardization: VDM’s base language was standardized as ISO/IEC 13817‑1:1996 (VDM‑SL).
- Tools and evolution: Tool support continued outside IBM via IFAD’s VDMTools and, later, the open‑source Overture platform. The notation was also extended to VDM++ (object‑oriented) and VDM‑RT (real‑time).
- Industrial/academic use: While Z (and later B) became popular in some UK/European organizations, VDM remained in use in industry and academia; it didn’t disappear so much as live on outside IBM’s walls.
If the exact name you saw internally wasn’t “VDM” or “Meta‑IV,” it may have been an IBM‑packaged course/tool around VDM, but the underlying language and method were those.
