Skip to content

Conversation

@JJWRoeloffs
Copy link
Contributor

@JJWRoeloffs JJWRoeloffs commented Oct 29, 2025

This pull request adds the detection of files used for the B formal method.

The B-method is a formal method for writing code that satisfies some formal mathematical description. You start with a mathematical machine (.mch), refine it in refinement steps (.ref), and finally end with an implementation (.imp), which can be transpiled into an executable programming language (such as C, ADA, or Rust.)

These files are not commonly checked into public github repositories, as the projects are generally either too academic or too corporate. This means the latter two extensions are on the border of acceptable of being added to linguist, with the most questionable being .ref, which has a little over two hundred files, most of which are in separate repositories as far as I can tell.

For the syntax highlighting, I had to write my own tmGrammar file, as none exist (though Vim does supports B without plugins,) which I did basing myself on the open B Language Reference, making a quick VSCode extension. I did this in one grammar file instead of three because the B Language Reference describes it like that.

I used the name B (Formal Method) to not confuse anyone about it being the predecessor of C, which is a different language called B. This B is a successor of Z.

Because machine, refinement (or reference) and implementation are not terms unique to B, the extensions are not either, even while no other users are in linguist currently. Because of this, I added some heuristics that should allow these extensions to only be classified as B when they are B, leaving them unclassified otherwise.

Checklist:

@JJWRoeloffs JJWRoeloffs requested a review from a team as a code owner October 29, 2025 13:57
@JJWRoeloffs JJWRoeloffs changed the title Add B (Formal Method) files Add B (Formal Method) language Oct 29, 2025
@JJWRoeloffs
Copy link
Contributor Author

JJWRoeloffs commented Oct 29, 2025

Fixing all my stuff to make the tests pass took me way longer than it should have. The documentation is way too good for me to make this many mistakes.


There are no other languages in linguist using .mch, .imp, or .ref, but a search of the files finds that all of these extensions are more commonly used outside of the B method, so I added heuristics. For each of those heuristics, my intent is to have the file only be classified as B if the regex pattern matches, else having it remain an unclassified file, but I did not find a way to test this working.

Looking at the way in which the other tests are written, I am really not sure if I did this correctly. In another pull request, you ask for the user to find another popular language with the extension to differentiate, but, in this case, .ref and .imp just mean "reference" and "implementation" and are used for all sorts of files. I am presuming Linguist has to have a feature for this if the way I did it is not correct, though I cannot find it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant